orderIsoIsTwoSided — Mathlib

English

A repeated statement that the Galois connection holds between fromIdeal and asIdeal.

Русский

Повторное утверждение существования сопряжения Галуа между fromIdeal и asIdeal.

LaTeX

$$$\mathrm{GaloisConnection}(\mathrm{fromIdeal}, \mathrm{asIdeal})$$$

Lean4

/-- A two-sided ideal is simply a left ideal that is two-sided. -/
@[simps]
def orderIsoIsTwoSided {R : Type*} [Ring R] : TwoSidedIdeal R ≃o { I : Ideal R // I.IsTwoSided }
    where
  toFun I := ⟨I.asIdeal, inferInstance⟩
  invFun
    I :=
    have := I.2;
    I.1.toTwoSided
  left_inv _ := by simp
  right_inv I := by simp
  map_rel_iff' {I I'} := by simp [SetLike.le_def]

Похожие утверждения