linear_toAffineMap — Mathlib

English

For an affine equivalence, the linear part of its toAffineMap matches its linear component.

Русский

У автономного аффинного эквивалента линейная часть отображения toAffineMap равна его линейному компоненту.

LaTeX

$$$\\mathrm{toAffineMap}(e)_{\\text{linear}} = e_{\\text{linear}}$$$

Lean4

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

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