cast_ne_one

Mathlib.Data.Int.Cast.Lemmas

URI: https://scilib.ai/kg/mathlib#Int.cast_ne_one

English

(n : α) ≠ 1 iff n ≠ 1.

Русский

(n : α) ≠ 1 эквивалентно n ≠ 1.

LaTeX

$$$ \forall {\alpha} [AddGroupWithOne \alpha] [CharZero \alpha],{n : \mathbb{Z}}, (n : \alpha) \neq 1 \iff n \neq 1$$$

Lean4

theorem cast_ne_one : (n : α) ≠ 1 ↔ n ≠ 1 :=
  cast_eq_one.not

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

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

Разделы

Аффилиация

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