neg_smul_equiv — Mathlib

English

If u is a unit, then W'.neg (u · P) is equivalent to W'.neg P under the natural equivalence of projective points.

Русский

Если u является единицей, то W'.neg (u · P) эквивалентна W'.neg P под естественным отношением эквивалентности проективных точек.

LaTeX

$$$$W'.neg (u \cdot P) \approx W'.neg P \quad (u \text{ unit})$$$$

Lean4

theorem neg_smul_equiv (P : Fin 3 → R) {u : R} (hu : IsUnit u) : W'.neg (u • P) ≈ W'.neg P :=
  ⟨hu.unit, (W'.neg_smul ..).symm⟩

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