ofNat_eq_top — Mathlib

English

For a commutative semiring R, and a natural n with n ≠ 0, the ideal n (as a principal ideal) equals ⊤.

Русский

Для коммутативного полугリングа R и натурального числа n, не равного нулю, идеал, порожденный n, равен ⊤.

LaTeX

$$$ n \neq 0 \Rightarrow (n : \mathrm{Ideal}\, R) = \top $$$

Lean4

/-- `3 : Ideal R` is *not* the ideal generated by 3 (which would be spelt
    `Ideal.span {3}`), it is simply `1 + 1 + 1 = ⊤`. -/
theorem ofNat_eq_top {n : ℕ} [n.AtLeastTwo] : (ofNat(n) : Ideal R) = ⊤ :=
  ofNat_eq_one.trans one_eq_top

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