symm_toRingEquiv — Mathlib

English

The inverse of an algebra equivalence, viewed as an additive equivalence, is the inverse additive equivalence of the original; i.e. the symm of e as an additive equivalence equals the inverse AddEquiv of e.

Русский

Обратная алгебровой эквивалентности, рассматриваемая как аддитивная эквивалентность, равна обратной аддитивной эквивалентности исходной; то есть symm(e) как аддитивная эквив. равна e^{-1} по аддитивной структуре.

LaTeX

$$$(e^{\mathrm{symm}} : A_2 \simeq_+ A_1) = (e : A_1 \simeq_+ A_2)^{-1}$$$

Lean4

@[simp]
theorem symm_toRingEquiv : (e.symm : A₂ ≃+* A₁) = (e : A₁ ≃+* A₂).symm :=
  rfl

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