equation_smul — Mathlib

English

Scaling a projective point by a unit preserves the equation.

Русский

Если точка P удовлетворяет проективному уравнению W'.Equation и u — единица в кольце, то умноженная на u точка u • P также удовлетворяет уравнению, и наоборот с учетом обратной единицы. Это выражает однородность кубического уравнения.

LaTeX

$$$W'.Equation(u \\cdot P) \\;\\;\\text{ iff }\\;\\; W'.Equation(P) \\\\text{ for unit } u$$

Lean4

theorem equation_smul (P : Fin 3 → R) {u : R} (hu : IsUnit u) : W'.Equation (u • P) ↔ W'.Equation P :=
  have hP (u : R) {P : Fin 3 → R} (hP : W'.Equation P) : W'.Equation <| u • P :=
    by
    rw [equation_iff] at hP ⊢
    linear_combination (norm := (simp only [smul_fin3_ext]; ring1)) u ^ 3 * hP
  ⟨fun h => by convert hP (↑hu.unit⁻¹) h; rw [smul_smul, hu.val_inv_mul, one_smul], hP u⟩

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