direction_smul — Mathlib

English

For a ≠ 0 in a field, the direction of a scaled subspace equals the original direction.

Русский

Для a ≠ 0 в поле направление масштабированного подпроcтранства совпадает с исходным направлением.

LaTeX

$$$ (a \\neq 0) \\rightarrow (a \\cdot s).direction = s.direction $$$

Lean4

@[simp]
theorem direction_smul (ha : a ≠ 0) (s : AffineSubspace k V) : (a • s).direction = s.direction :=
  by
  have : DistribMulAction.toLinearMap k V a = a • LinearMap.id := by ext; simp
  simp [smul_eq_map, map_direction, this, Submodule.map_smul, ha]

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