algEquivOfAlgEquiv_symm — Mathlib

English

Equality of algEquivOfAlgEquiv as x varies: eq on the algebra map commutes with the isomorphism.

Русский

Равенство AlgEquivOfAlgEquiv при изменении x сохраняется через композицию отображений.

LaTeX

$$$\\mathrm{algEquivOfAlgEquiv}(S,Q,h,H)(\\mathrm{algebraMap}_R^S x) = \\mathrm{algebraMap}_P^Q (h x)$$$

Lean4

theorem algEquivOfAlgEquiv_symm :
    (algEquivOfAlgEquiv S Q h H).symm =
      algEquivOfAlgEquiv Q S h.symm
        (show Submonoid.map h.symm T = M by
          rw [← H, ← Submonoid.map_coe_toMulEquiv, AlgEquiv.symm_toMulEquiv, ← Submonoid.comap_equiv_eq_map_symm, ←
            Submonoid.map_coe_toMulEquiv, Submonoid.comap_map_eq_of_injective (h : R ≃* P).injective]) :=
  rfl

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