toLinearEquiv_toLinearMap — Mathlib

English

The two representations of an equivalence as a linear map and as a linear equivalence coincide, i.e., the linear map underlying the equivalence matches its linear-equivalence form.

Русский

Две записи эквивалентности как линейного отображения и как линейной эквивалентности совпадают; линейное отображение внутри эквивалентности совпадает с формой линейной эквив.\n

LaTeX

$$$ ((e : A \\simeq_{\\ell_c[R]} B) : A \\to B) = (e : A \\to_{?} B) $$$

Lean4

theorem toLinearEquiv_toLinearMap : ((e : A ≃ₗ[R] B) : A →ₗ[R] B) = (e : A →ₗc[R] B) :=
  rfl

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