one_ne_ofNat

Mathlib.Algebra.CharZero.Defs

URI: https://scilib.ai/kg/mathlib#OfNat.one_ne_ofNat

English

Let R be as above. Then for every n with n ≥ 2, 1 ≠ (n : R).

Русский

Пусть R удовлетворяет указанным условиям. Тогда для каждого n ≥ 2 выполняется 1 ≠ (n : R).

LaTeX

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

Lean4

@[simp]
theorem one_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (1 : R) ≠ ofNat(n) :=
  (ofNat_ne_one n).symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru