FormalConjecturesForMathlib/RingTheory/Ideal/Maximal.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

8 declarations, 0 contain sorry, 0 declared as axioms

Maximal right ideals

This file defines maximal right ideals and gives their basic order-theoretic API.

Imports (2)
Imported by 1 file
  1. class RightIdeal.IsMaximal A right ideal is maximal if it is maximal among the proper right ideals line 38 source

    Source documentation

    A right ideal is maximal if it is maximal among the proper right ideals.

    standard axioms: Quot.sound, propext what this means

    Statement uses: Semiring, RightIdeal

    class IsMaximal : Prop where
…
  2. theorem RightIdeal.isMaximal_def line 42 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Semiring, RightIdeal, Iff, RightIdeal.IsMaximal, IsCoatom, MulOpposite

    Proof uses: Iff.intro, RightIdeal.IsMaximal.out, RightIdeal.IsMaximal.mk

    12 instances, coercions and auxiliary constants left out.

  3. theorem RightIdeal.IsMaximal.ne_top line 45 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Semiring, RightIdeal, RightIdeal.IsMaximal, Ne, Top.top, MulOpposite

    Proof uses: And.left, LT.lt, Eq, Iff.mp, IsCoatom, RightIdeal.isMaximal_def

    13 instances, coercions and auxiliary constants left out.

  4. theorem RightIdeal.IsMaximal.lt_top line 48 source

    standard axioms: Quot.sound, propext what this means

    Statement uses: Semiring, RightIdeal, RightIdeal.IsMaximal, LT.lt, MulOpposite, Top.top

    Proof uses: Ne.lt_top, RightIdeal.IsMaximal.ne_top

    12 instances, coercions and auxiliary constants left out.

  5. theorem RightIdeal.IsMaximal.eq_of_le line 51 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Semiring, RightIdeal, RightIdeal.IsMaximal, Ne, Top.top, MulOpposite, LE.le, Eq

    Proof uses: Iff.mpr, And, Not, LT.lt, eq_iff_le_not_lt, And.intro, And.right, Iff.mp, IsCoatom, RightIdeal.isMaximal_def

    17 instances, coercions and auxiliary constants left out.

  6. theorem RightIdeal.IsMaximal.eq_iff_le line 56 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Semiring, RightIdeal, RightIdeal.IsMaximal, Ne, Top.top, MulOpposite, Iff, Eq, LE.le

    Proof uses: Iff.intro, Eq.le, RightIdeal.IsMaximal.eq_of_le

    14 instances, coercions and auxiliary constants left out.

  7. theorem RightIdeal.isMaximal_toIdeal_iff line 67 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: CommSemiring, RightIdeal, Iff, Ideal.IsMaximal, RightIdeal.toIdeal, RightIdeal.IsMaximal

    Proof uses: Eq.mpr, IsCoatom, Ideal, id, Eq, congrArg, propext, Ideal.isMaximal_def, MulOpposite, RightIdeal.isMaximal_def, OrderIso.isCoatom_iff, RightIdeal.orderIsoIdeal

    9 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  8. theorem RightIdeal._root_.Ideal.isMaximal_toRightIdeal_iff line 72 source