cast_to_num

Mathlib.Data.Num.Lemmas

URI: https://scilib.ai/kg/mathlib#PosNum.cast_to_num

English

Casting a positive numeral to Num yields the same numeral as Num.pos.

Русский

Пусть положимое число в PosNum приводится к Num тем же числом (Num.pos).

LaTeX

$$$\\forall n \\in \\text{PosNum},\\; \\uparrow n = \\operatorname{Num.pos} n$$$

Lean4

@[simp]
theorem cast_to_num (n : PosNum) : ↑n = Num.pos n := by rw [← cast_to_nat, ← of_to_nat n]

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

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

Разделы

Аффилиация

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