English
Explicit formula for polynomialZ: W'.polynomialZ equals Y^2 + a1 X Y + 2 a3 Y Z − (a2 X^2 + 2 a4 X Z + 3 a6 Z^2).
Русский
Явная формула для polynomialZ: W'.polynomialZ = Y^2 + a1 X Y + 2 a3 Y Z − (a2 X^2 + 2 a4 X Z + 3 a6 Z^2).
LaTeX
$$$W'.polynomialZ = Y^2 + W'.a_1 \\cdot X \\cdot Y + 2 W'.a_3 \\cdot Y \\cdot Z - (W'.a_2 \\cdot X^{2} + 2 W'.a_4 \\cdot X \\cdot Z + 3 W'.a_6 \\cdot Z^{2})$$$
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 ^ 2 * hP'.left, by
linear_combination (norm := ring1) u ^ 2 * hP'.right.left, by
linear_combination (norm := ring1) u ^ 2 * hP'.right.right⟩
⟨hP hu, fun h => hP hu.unit⁻¹.isUnit <| by rwa [smul_smul, hu.val_inv_mul, one_smul]⟩
