cast_to_nat — Mathlib

English

For any AddMonoidWithOne α, every PosNum n satisfies ((n : ℕ) : α) = n.

Русский

Для любого AddMonoidWithOne α каждый PosNum n удовлетворяет ((n : ℕ) : α) = n.

LaTeX

$$$\\forall \\alpha\\;[\\mathrm{AddMonoidWithOne}\\;\\alpha],\\;\\forall n:\\mathrm{PosNum}, ((n : \\mathbb{N}) : \\alpha) = n$$$

Lean4

@[simp, norm_cast]
theorem cast_to_nat [AddMonoidWithOne α] : ∀ n : PosNum, ((n : ℕ) : α) = n
  | 1 => Nat.cast_one
  | bit0 p => by dsimp; rw [Nat.cast_add, p.cast_to_nat]
  | bit1 p => by dsimp; rw [Nat.cast_add, Nat.cast_add, Nat.cast_one, p.cast_to_nat]

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