cast_to_nat — Mathlib

English

For any α with AddMonoidWithOne, the embedding of Num into α via the natural numbers commutes with the Num embedding: for all n, ((n : ℕ) : α) = n.

Русский

Для любого α с структурой AddMonoidWithOne вложение Num в α через натуральные числа согласуется с вложением самого Num: для всех n, ((n : ℕ) : α) = n.

LaTeX

$$$\\forall n : Num, ((n : \\mathbb{N}) : \\alpha) = n$$$

Lean4

@[simp, norm_cast]
theorem cast_to_nat [AddMonoidWithOne α] : ∀ n : Num, ((n : ℕ) : α) = n
  | 0 => Nat.cast_zero
  | pos p => p.cast_to_nat

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