natSize_to_nat

Mathlib.Data.Num.Lemmas

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

English

natSize n = Nat.size n for all PosNum n.

Русский

natSize n = Nat.size n для всех PosNum n.

LaTeX

$$$ natSize\, n = Nat.size\, n $$$

Lean4

theorem natSize_to_nat (n) : natSize n = Nat.size n := by rw [← size_eq_natSize, size_to_nat]

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

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

Разделы

Аффилиация

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