equation_of_equiv — Mathlib

English

If P ≈ Q (P and Q represent the same point in the Jacobian class), then W'.Equation P holds if and only if W'.Equation Q holds.

Русский

Если P ≈ Q (P и Q представляют одну и ту же точку в классе Якобиана), то верно W'.Equation P тогда и только тогда, когда верно W'.Equation Q.

LaTeX

$$$\\forall P,Q:\\ Fin(3) \\to R,\\; P \\approx Q \\Rightarrow (W'.Equation(P) \\iff W'.Equation(Q))$$$

Lean4

theorem equation_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W'.Equation P ↔ W'.Equation Q :=
  by
  rcases h with ⟨u, rfl⟩
  exact equation_smul Q u.isUnit

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