English
Multiplying the coordinate triple P by a unit u preserves the nonsingularity, i.e., W'.Nonsingular (u • P) ⇔ W'.Nonsingular P.
Русский
Умножение тройки координат на единицу сохраняет неособость: W'.Nonsingular (u • P) ⇔ W'.Nonsingular P, если u — единица.
LaTeX
$$$ W'.Nonsingular (u \\cdot P) \\;\\iff\\; W'.Nonsingular P , \\;\\text{for } u \\text{ a unit}$$$
Lean4
theorem nonsingular_smul (P : Fin 3 → R) {u : R} (hu : IsUnit u) : W'.Nonsingular (u • P) ↔ W'.Nonsingular P :=
have hP {u : R} (hu : IsUnit u) {P : Fin 3 → R} (hP : W'.Nonsingular <| u • P) : W'.Nonsingular P :=
by
rcases (nonsingular_iff _).mp hP with ⟨hP, hP'⟩
refine (nonsingular_iff P).mpr ⟨(equation_smul P hu).mp hP, ?_⟩
contrapose! hP'
simp only [smul_fin3_ext]
exact
⟨by linear_combination (norm := ring1) u ^ 4 * hP'.left, by
linear_combination (norm := ring1) u ^ 3 * hP'.right.left, by
linear_combination (norm := ring1) u ^ 5 * hP'.right.right⟩
⟨hP hu, fun h => hP hu.unit⁻¹.isUnit <| by rwa [smul_smul, hu.val_inv_mul, one_smul]⟩
