coe_toAffineMap

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

URI: https://scilib.ai/kg/mathlib#AffineEquiv.coe_toAffineMap

English

The underlying function of the affine map e.toAffineMap is the same as the function e.

Русский

Функция, лежащая в основе отображения e.toAffineMap, совпадает с функцией e.

LaTeX

$$$(e.toAffineMap : P_1 \to P_2) = (e : P_1 \to P_2)$$$

Lean4

@[simp]
theorem coe_toAffineMap (e : P₁ ≃ᵃ[k] P₂) : (e.toAffineMap : P₁ → P₂) = (e : P₁ → P₂) :=
  rfl

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

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

Разделы

Аффилиация

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