cast_pow — Mathlib

English

For any ring R and integers n and natural m, the cast of n^m equals (n^m) in R of n: ↑(n^m) = (n^m : R) = (n : R)^m.

Русский

Для кольца R и целых n, натурального m верна равенство: ↑(n^m) = (n^m : R) = (n : R)^m.

LaTeX

$$$\uparrow\!(n^{m}) = (n^{m} : R) = (n : R)^{\,m}$$$

Lean4

@[simp, norm_cast]
theorem cast_pow {R : Type*} [Ring R] (n : ℤ) (m : ℕ) : ↑(n ^ m) = (n ^ m : R) := by
  induction m <;> simp [_root_.pow_succ, *]

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