cast_eq_one

Mathlib.Data.Int.Cast.Lemmas

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem cast_eq_one : (n : α) = 1 ↔ n = 1 := by rw [← cast_one, cast_inj]

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

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

Разделы

Аффилиация

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