fst_natCast

Mathlib.Data.Nat.Cast.Prod

URI: https://scilib.ai/kg/mathlib#Prod.fst_natCast

English

Casting a natural number into the product α × β, its first component is the same natural number.

Русский

При отображении натурального числа в произведение α × β его первая компонента равна этому числу.

LaTeX

$$$ (n : α \times β).\mathrm{fst} = n $$$

Lean4

@[simp]
theorem fst_natCast (n : ℕ) : (n : α × β).fst = n := by induction n <;> simp [*]

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

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

Разделы

Аффилиация

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