symm_toMulEquiv — Mathlib

English

For a given algebra equivalence e: A1 ≃ₐ[R] A2, the symmetric multiplicative equivalence equals the multiplicative equivalence of the symmetric version; i.e. (e.symm) as a ring/mul equivalence equals (e) as a ring/mul equivalence, reversed.

Русский

Симметричная мультипликативная эквивалентность равна обратной мультипликативной эквивалентности исходной; то есть симм-представление эквив. совпадает с обратным эквивалентом.

LaTeX

$$$(e^{\mathrm{symm}} : A_2 \simeq_* A_1) = (e : A_1 \simeq_* A_2).\mathrm{symm}$$$

Lean4

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

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