forall_eq_iff_forall_eq — Mathlib

English

For a semiring R, the statement that all polynomials are equal is equivalent to the statement that all elements of R are equal.

Русский

Для полей R: равенство всех полиномов эквивалентно равенству всех элементов R.

LaTeX

$$$(\forall f,g : \operatorname{Polynomial}(R), f=g) \iff (\forall a,b : R, a=b)$$$

Lean4

theorem forall_eq_iff_forall_eq : (∀ f g : R[X], f = g) ↔ ∀ a b : R, a = b := by
  simpa only [← subsingleton_iff] using subsingleton_iff_subsingleton

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