pow_mem_graded — Mathlib

English

If r ∈ A i, then r^n ∈ A (n • i) for any n.

Русский

Если r ∈ A i, то r^n ∈ A (n • i) для любого n.

LaTeX

$$$\\forall n\\in\\mathbb{N},\\ r\\in A i:\\ r^n \\in A (n\\cdot i)$$$

Lean4

theorem pow_mem_graded (n : ℕ) {r : R} {i : ι} (h : r ∈ A i) : r ^ n ∈ A (n • i) := by
  match n with
  | 0 =>
    rw [pow_zero, zero_nsmul]
    exact one_mem_graded _
  | n + 1 =>
    rw [pow_succ', succ_nsmul']
    exact mul_mem_graded h (pow_mem_graded n h)

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