coe_linear — Mathlib

English

The linear part of the affine map associated to an affine equivalence matches the given linear part of the equivalence.

Русский

Линейная часть аффинного отображения, связанная с аффинным эквивалентом, совпадает с данной линейной частью эквивалентности.

LaTeX

$$$(e.toAffineMap).linear = e.linear$$$

Lean4

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

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