ofNat_ne_one — Mathlib

English

Let R be a additive monoid with one and characteristic zero. If n is a natural number with n ≥ 2, then its image in R is not equal to 1.

Русский

Пусть R — аддитивный моноид с единицей и характеристика равна нулю. Для натурального числа n ≥ 2 образ числа n в R не равен единице.

LaTeX

$$$ \forall n \in \mathbb{N},\ n \ge 2 \Rightarrow (n : R) \neq 1 $$$

Lean4

@[simp]
theorem ofNat_ne_one (n : ℕ) [n.AtLeastTwo] : (ofNat(n) : R) ≠ 1 :=
  Nat.cast_ne_one.2 (Nat.AtLeastTwo.ne_one)

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