coe_toLinearEquiv — Mathlib

English

The map from an additive equivalence to its linear equivalence is compatible with scalar action; its underlying function is the same.

Русский

Отображение от аддитивного эквивалента к линейному эквиваленту совместимо с действием скаляров; базовая функция одинакова.

LaTeX

$$$ (e.toLinearEquiv h) \text{ coe } = e $$$

Lean4

@[simp]
theorem coe_toLinearEquiv (h : ∀ (c : R) (x), e (c • x) = c • e x) : ⇑(e.toLinearEquiv h) = e :=
  rfl

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