symm_toAddEquiv — Mathlib

English

The symm of an algebra equivalence as a multiplicative equivalence coincides with the multiplicative equivalence induced by the inverse algebra equivalence.

Русский

Симметричная мультипликативная эквивалентность алгебровой эквивалентности совпадает с мультипликативной эквивалентностью, порожденной обратной алгебровой эквивалентностью.

LaTeX

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

Lean4

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

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