toLinearEquiv_refl — Mathlib

English

The linear equivalence obtained from the reflexive algebra equivalence is the identity linear equivalence.

Русский

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

LaTeX

$$$\\text{toLinearEquiv}(\\mathrm{refl}) = \\mathrm{LinearEquiv.refl}$$$

Lean4

@[simp]
theorem toLinearEquiv_refl : (AlgEquiv.refl : A₁ ≃ₐ[R] A₁).toLinearEquiv = LinearEquiv.refl R A₁ :=
  rfl

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