toLinearEquiv_eq_coe — Mathlib

English

For any e: A ≃ₗc[R] B, its linear equivalence part equals the linear part of e, i.e., e.toLinearEquiv equals the canonical linear structure of e.

Русский

Для любой e: A ≃ₗc[R] B линейная эквивалентность e равна линейной части e; т.е. e.toLinearEquiv совпадает с канонической линейной структурой e.

LaTeX

$$$ e.toLinearEquiv = e $$$

Lean4

@[simp]
theorem toLinearEquiv_eq_coe (f : A ≃ₗc[R] B) : f.toLinearEquiv = f :=
  rfl

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