ringEquivOfRingEquiv_symm — Mathlib

English

The inverse isomorphism corresponds to the inverse ring equivalence with the corresponding monoid map equivalence.

Русский

Обратный изоморфизм соответствует обратному кольцевому эквиваленту и соответствующему эквиваленту по моноиду.

LaTeX

$$$$ (\\mathrm{ringEquivOfRingEquiv}(S,Q,j,H))^{-1} = \\mathrm{ringEquivOfRingEquiv}(Q,S,j^{-1},\\text{appropriate }H') $$$$

Lean4

@[simp]
theorem ringEquivOfRingEquiv_symm {j : R ≃+* P} (H : M.map j = T) :
    (ringEquivOfRingEquiv S Q j H).symm =
      ringEquivOfRingEquiv Q S j.symm
        (show T.map (j : R ≃* P).symm = M by
          rw [← H, ← Submonoid.comap_equiv_eq_map_symm, ← Submonoid.map_coe_toMulEquiv,
            Submonoid.comap_map_eq_of_injective (j : R ≃* P).injective]) :=
  rfl

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