English
For any P ∈ Fin(3) → R and any unit u ∈ R, the scaled triple u • P satisfies the Weierstrass equation on W' if and only if P does.
Русский
Для любой P ∈ Fin(3) → R и любого единичного элемента u ∈ R тождественный тройка u · P удовлетворяет уравнению Вейерштрасса на W' тогда и только тогда, когда удовлетворяет P.
LaTeX
$$$W'.Equation(u\\cdot P) \\iff W'.Equation(P)$ при \\(u \\in R^\times\\)$$
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 ^ 6 * hP
⟨fun h => by convert hP (↑hu.unit⁻¹) h; rw [smul_smul, hu.val_inv_mul, one_smul], hP u⟩