units_smul_of_pos — Mathlib

English

Scaling a ray by a positive unit leaves it unchanged. If u ∈ Rˣ with u>0 and v is a ray, then u • v = v.

Русский

Умножение луча положительной единицей не меняет луча. Пусть u ∈ Rˣ и u>0; тогда u • v = v.

LaTeX

$$$u\cdot v = v\quad\text{for } u\in R^{\times},\ 0< (u:R).$$$

Lean4

/-- Scaling by a positive unit is a no-op. -/
theorem units_smul_of_pos (u : Rˣ) (hu : 0 < (u : R)) (v : Module.Ray R M) : u • v = v :=
  by
  induction v using Module.Ray.ind
  rw [smul_rayOfNeZero, ray_eq_iff]
  exact SameRay.sameRay_pos_smul_left _ hu

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