English
For a NonAssocRing R with Pow by ℕ and NatPowAssoc, and for any n ∈ ℤ, (n^m) cast to R equals (n cast)^m for all m ∈ ℕ.
Русский
Пусть R — неассоциированное кольцо, с мощностью по ℕ и NatPowAssoc. Тогда для любого n ∈ ℤ выполняется (n^m) как элемент R равно (n как элемент R)^m для всех m ∈ ℕ.
LaTeX
$$$ \forall (n \in \mathbb{Z}), (\mathrm{Int.cast}_R(n^m)) = (n^R)^m, \forall m \in \mathbb{N}$$$
Lean4
@[simp, norm_cast]
theorem cast_npow (R : Type*) [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (n : ℤ) :
∀ (m : ℕ), @Int.cast R NonAssocRing.toIntCast (n ^ m) = (n : R) ^ m
| 0 => by rw [pow_zero, npow_zero, Int.cast_one]
| m + 1 => by rw [npow_add, npow_one, Int.cast_mul, Int.cast_npow R n m, npow_add, npow_one]
