equiv_iff_eq_of_Z_eq — Mathlib

English

Over a NoZeroDivisors ring R, for P, Q: Fin 3 → R, if P 2 = Q 2 and Q 2 ∈ nonZeroDivisors R, then P ≈ Q if and only if P = Q.

Русский

В кольце без нулевых делителей R для P, Q: Fin 3 → R, если P(2) = Q(2) и Q(2) ∈ nonZeroDivisors R, то P ≈ Q тогда и только тогда, когда P = Q.

LaTeX

$$P ≈ Q ↔ P = Q$$

Lean4

theorem equiv_iff_eq_of_Z_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hz : P z = Q z) (hQz : Q z ≠ 0) : P ≈ Q ↔ P = Q :=
  equiv_iff_eq_of_Z_eq' hz <| mem_nonZeroDivisors_of_ne_zero hQz

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