coe_ofLinearEquiv

Mathlib.LinearAlgebra.GeneralLinearGroup

URI: https://scilib.ai/kg/mathlib#LinearMap.GeneralLinearGroup.coe_ofLinearEquiv

English

The image of a linear equivalence under the embedding equals the underlying linear map.

Русский

Изображение линейной эквивалентности под инъекцией равно базовой линейной карте.

LaTeX

$$$\mathrm{coe\_ofLinearEquiv}: \mathrm{ofLinearEquiv}(f) = f$$$

Lean4

@[simp]
theorem coe_ofLinearEquiv (f : M ≃ₗ[R] M) : ofLinearEquiv f = (f : M → M) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru