monic_zero_iff_subsingleton' — Mathlib

English

Monic 0 is equivalent to the conjunction of universal equalities: every pair of polynomials are equal and every pair of coefficients are equal.

Русский

Монничность нулевого полиномa эквивалентна сочетанию всеобщих равенств: любые два полинома равны и любые две коэффициенты равны.

LaTeX

$$$\operatorname{Monic}(0) \iff (\forall f,g:\, R[X],\ f=g) \land (\forall a,b:\, R,\ a=b).$$$

Lean4

theorem monic_zero_iff_subsingleton' : Monic (0 : R[X]) ↔ (∀ f g : R[X], f = g) ∧ ∀ a b : R, a = b :=
  Polynomial.monic_zero_iff_subsingleton.trans
    ⟨by
      intro
      simp [eq_iff_true_of_subsingleton], fun h => subsingleton_iff.mpr h.2⟩

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