negDblY_of_Y_eq — Mathlib

English

If P lies on W and certain Y-equalities hold with Q, then negDblY P equals the negation of 2P’s X-related expression; i.e., negDblY P = -W.dblU P in a suitable sense.

Русский

Если P лежит на W и соблюдены Y-равенства относительно некоторой Q, то negDblY P выражается как отрицание dblU P.

LaTeX

$$$ {P,Q: Fin 3→F} (hP: W'.Equation P) (hQ: W'.Equation Q) \Rightarrow W'.negDblY P = -W'.dblU P$$$

Lean4

theorem negDblY_of_Y_eq {P Q : Fin 3 → F} (hP : W.Equation P) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z = Q x * P z) (hy : P y * Q z = Q y * P z) (hy' : P y * Q z = W.negY Q * P z) :
    W.negDblY P = -W.dblU P := by
  rw [dblU, ← neg_div, ← negDblY_of_Y_eq' hP hQz hx hy hy', mul_div_cancel_right₀ _ <| pow_ne_zero 2 hPz]

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