English
Let W' be the Jacobian of a Weierstrass curve over a commutative ring R. For any P: Fin_3 → R and any unit u ∈ R, the element W'.neg(u · P) is equivalent to W'.neg P under the induced equivalence relation; i.e., negation commutes with unit-scaling up to equivalence.
Русский
Пусть W' — касательная Якобиан к кривой Вейерштрасса над кольцом R. Для любого P: Fin_3 → R и любого единичного элемента u ∈ R элемент W'.neg(u · P) эквивалентен W'.neg P относительно соответствующей эквивалентности; то есть отрицание коммутирует с умножением на единицу до эквивалентности.
LaTeX
$$$\forall R\ [\text{CommRing }R],\ \forall {W' : \mathrm{Jacobian}(R)},\ \forall P : \mathrm{Fin}_3 \to R,\ \forall u \in R^{\times},\ W'.\neg (u \cdot P) \approx W'.\neg P$$$
Lean4
theorem neg_smul_equiv (P : Fin 3 → R) {u : R} (hu : IsUnit u) : W'.neg (u • P) ≈ W'.neg P :=
⟨hu.unit, (W'.neg_smul ..).symm⟩
