English
Under NoZeroDivisors, if P,Q satisfy the Y-relations (including hy'), and the other cross-relations hx, hy, hy', then W.dblZ P is a unit in the base field: IsUnit(W.dblZ P).
Русский
При NoZeroDivisors, если P,Q удовлетворяют Y-отношениям (включая hy'), а также hx, hy, hy', то W.dblZ P является единицей базы: IsUnit(W.dblZ P).
LaTeX
$$$ [NoZeroDivisors\ R] \; {P,Q}: W'.Equation P, W'.Equation Q, P_z ≠ 0, Q_z ≠ 0, hx, hy, hy' \Rightarrow IsUnit(W'.dblZ P)$$$
Lean4
theorem dblX_eq' {P : Fin 3 → R} (hP : W'.Equation P) :
W'.dblX P * P z =
(eval P W'.polynomialX ^ 2 - W'.a₁ * eval P W'.polynomialX * P z * (P y - W'.negY P) -
W'.a₂ * P z ^ 2 * (P y - W'.negY P) ^ 2 -
2 * P x * P z * (P y - W'.negY P) ^ 2) *
(P y - W'.negY P) :=
by
linear_combination (norm := (rw [dblX, eval_polynomialX, negY]; ring1))
9 * (W'.a₁ * P x ^ 2 + 2 * P x * P y) * (equation_iff _).mp hP
