toAffineMap_mk

Mathlib.LinearAlgebra.AffineSpace.AffineEquiv

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

English

For f, f' and h, toAffineMap (mk f f' h) equals ⟨f, f', h⟩.

Русский

Для отображений f, f' и h, toAffineMap (mk f f' h) равно ⟨f, f', h⟩.

LaTeX

$$$\\mathrm{toAffineMap}(\\mathrm{mk} f\\; f'\\; h) = \\langle f, f', h \\rangle$$$

Lean4

@[simp]
theorem toAffineMap_mk (f : P₁ ≃ P₂) (f' : V₁ ≃ₗ[k] V₂) (h) : toAffineMap (mk f f' h) = ⟨f, f', h⟩ :=
  rfl

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

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

Разделы

Аффилиация

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