LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Operations #
Imported Lean Pool material for
LeanPool.BrauerGroupNew.Mathlib.RingTheory.TwoSidedIdeal.Operations.
theorem
TwoSidedIdeal.comap_injective
{F : Type u_1}
{R : Type u_2}
{S : Type u_3}
[Ring R]
[Ring S]
[FunLike F R S]
[RingHomClass F R S]
(f : F)
(hf : Function.Surjective ⇑f)
:
Function.Injective ⇑(comap f)
def
TwoSidedIdeal.orderIsoOfRingEquiv
{R : Type u_2}
{S : Type u_3}
[Ring R]
[Ring S]
{F : Type u_4}
[EquivLike F R S]
[RingEquivClass F R S]
(f : F)
:
The order isomorphism on two-sided ideals induced by a ring equivalence.
Equations
- TwoSidedIdeal.orderIsoOfRingEquiv f = { toFun := ⇑(TwoSidedIdeal.comap (↑f).symm), invFun := ⇑(TwoSidedIdeal.comap ↑f), left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }