dblY_of_Y_eq — Mathlib

English

Under NoZeroDivisors and certain proportional relations between P and Q, negDblY P equals (−dblU P)^3.

Русский

При отсутствии нулевых делителей и заданных пропорциональных условиях между P и Q, negDblY(P) = (−dblU(P))^3.

LaTeX

$$Same as above with NoZeroDivisors and P, Q conditions$$

Lean4

theorem dblY_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2)
    (hy : P y * Q z ^ 3 = Q y * P z ^ 3) (hy' : P y * Q z ^ 3 = W'.negY Q * P z ^ 3) : W'.dblY P = W'.dblU P ^ 3 :=
  by
  rw [dblY, negY_eq, negDblY_of_Y_eq hQz hx hy hy', dblZ_of_Y_eq hQz hx hy hy']
  ring1

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