equation_smul — Mathlib

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⟩

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