coeffsIn_pow — Mathlib

English

For any natural number n ≠ 0, coeffsIn σ M raised to the power n is contained in coeffsIn σ M raised to the power n: coeffsIn σ M^n ≤ (coeffsIn σ M)^n.

Русский

Для любого натурального n ≠ 0: coeffsIn σ M^n ≤ coeffsIn σ M)^n.

LaTeX

$$$\\operatorname{coeffsIn}(\\sigma, M)^{n} = ? \\quad \\text{(in the context of powers, the lemma asserts a monotonic relation)}$$$

Lean4

theorem coeffsIn_pow : ∀ {n}, n ≠ 0 → ∀ M : Submodule R S, coeffsIn σ (M ^ n) = coeffsIn σ M ^ n
  | 1, _, M => by simp
  | n + 2, _, M => by rw [pow_succ, coeffsIn_mul, coeffsIn_pow, ← pow_succ]; exact n.succ_ne_zero

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