symm — Mathlib

English

The double symmetry of an algebra equivalence yields the original equivalence.

Русский

Двойная симметрия алгебраической эквивалентности возвращает исходную эквивалентность.

LaTeX

$$$ e^{\text{symm} \text{symm}} = e $$$

Lean4

/-- Algebra equivalences are symmetric. -/
@[symm]
def symm (e : A₁ ≃ₐ[R] A₂) : A₂ ≃ₐ[R] A₁ :=
  { e.toRingEquiv.symm with
    commutes' := fun r => by
      rw [← e.toRingEquiv.symm_apply_apply (algebraMap R A₁ r)]
      congr
      simp }

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