1. FormalConjecturesForMathlib
  2. RingTheory
  3. Ideal
  4. Basic
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import FormalConjecturesForMathlib.RingTheory.Ideal.Defs public import Mathlib.RingTheory.Ideal.Defs

Right ideals

This file gives the basic API for right ideals.

@[expose] public sectionuniverse unamespace RightIdealsection Semiringvariable {R : Type u} [Semiring R]@[ext] theorem ext {I J : RightIdeal R} (h : ∀ x, x ∈ I ↔ x ∈ J) : I = J := Submodule.ext h

A right ideal is closed under multiplication on the right.

theorem mul_mem_right (I : RightIdeal R) {a : R} (b : R) (ha : a ∈ I) : a * b ∈ I := I.smul_mem (MulOpposite.op b) haend Semiringsection CommSemiringvariable {R : Type u} [CommSemiring R]

A right ideal in a commutative semiring, regarded as an ideal.

R:Type uinst✝:CommSemiring RI:RightIdeal Rr:Rx:Rhx:x ∈ ↑I⊢ x * r ∈ ↑I All goals completed! 🐙@[simp] theorem mem_toIdeal {I : RightIdeal R} {x : R} : x ∈ I.toIdeal ↔ x ∈ I := Iff.rfl

An ideal in a commutative semiring, regarded as a right ideal.

R:Type uinst✝:CommSemiring RI:Ideal Rr:Rᵐᵒᵖx:Rhx:x ∈ ↑I⊢ MulOpposite.unop r * x ∈ ↑I All goals completed! 🐙@[simp] theorem _root_.Ideal.mem_toRightIdeal {I : Ideal R} {x : R} : x ∈ I.toRightIdeal ↔ x ∈ I := Iff.rfl@[simp] theorem toIdeal_toRightIdeal (I : RightIdeal R) : I.toIdeal.toRightIdeal = I := rfl@[simp] theorem _root_.Ideal.toRightIdeal_toIdeal (I : Ideal R) : I.toRightIdeal.toIdeal = I := rfl

Over a commutative semiring, right ideals and ideals are order isomorphic.

def orderIsoIdeal (R : Type u) [CommSemiring R] : RightIdeal R ≃o Ideal R where toFun := toIdeal invFun := Ideal.toRightIdeal left_inv := toIdeal_toRightIdeal right_inv := Ideal.toRightIdeal_toIdeal map_rel_iff' := Iff.rflend CommSemiringend RightIdeal