eqZero — Mathlib

English

For natural number n, the sentence eqZero(n) expresses that n equals zero in the ring language.

Русский

Для натурального числа n предложение eqZero(n) выражает, что n равно нулю в языке колец.

LaTeX

$$eqZero(n) := \text{Term.equal} (\text{termOfFreeCommRing } n) 0$$

Lean4

/-- For a given natural number `n`, `eqZero n` is the sentence in the language of rings
saying that `n` is zero. -/
noncomputable def eqZero (n : ℕ) : Language.ring.Sentence :=
  Term.equal (termOfFreeCommRing n) 0

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