English
If R and S are rings isomorphic via e, then there is an order isomorphism between the two-sided ideals of R and those of S, given by the preimage under e.
Русский
Если кольца R и S изоморфны через e, то существует упорядоченный изоморфизм множеств двусторонних идеалов R и S, задаваемый через обратный образ по e.
LaTeX
$$$\\operatorname{TwoSidedIdeal}(R) \\cong_{o} \\operatorname{TwoSidedIdeal}(S)$, реализуемый через $I \\mapsto \\operatorname{comap}_e(I)$$$
Lean4
/-- If `R` and `S` are isomorphic as rings, then two-sided ideals of `R` and two-sided ideals of `S` are
order isomorphic.
-/
def _root_.RingEquiv.mapTwoSidedIdeal (e : R ≃+* S) : TwoSidedIdeal R ≃o TwoSidedIdeal S :=
OrderIso.ofHomInv (comap e.symm) (comap e) (by ext; simp [mem_comap]) (by ext; simp [mem_comap])
