neg_equiv — Mathlib

English

If P and Q are equivalent under the Fin_3 index relation, then the negations are equivalent: W'.neg P ≈ W'.neg Q.

Русский

Если P и Q эквивалентны по отношению на Fin_3, то отрицания эквивалентны: W'.neg P ≈ W'.neg Q.

LaTeX

$$$\forall {R : Type},\ [\text{CommRing }R],\ \forall {W' : \mathrm{Jacobian}(R)},\ \forall P,Q : \mathrm{Fin}_3 \to R,\ P \approx Q \Rightarrow W'.\neg P \approx W'.\neg Q$$$

Lean4

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

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