coe_symm_toLinearEquiv — Mathlib

English

If e,e' are algebra equivalences, then the transported equivalence is symmetric in its arguments.

Русский

Если e, e' — эквивалентности алгебр, то переносная эквивалентность симметрична в аргументах.

LaTeX

$$$\\text{equivCongr }(e,e')^{\\mathrm{symm}} = \\text{equivCongr }(e^{-1},(e')^{-1})$$$

Lean4

@[simp]
theorem coe_symm_toLinearEquiv (e : A₁ ≃ₐ[R] A₂) : ⇑e.toLinearEquiv.symm = e.symm :=
  rfl

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