pow — Mathlib

English

For a fractional submodule I, all powers I^n are fractional for every n ∈ N.

Русский

Для дробного подмодуля I все степени I^n дробны для каждого n ∈ N.

LaTeX

$$$\forall n \in \mathbb{N}, IsFractional S I \to IsFractional S (I^n)$$$

Lean4

theorem _root_.IsFractional.pow {I : Submodule R P} (h : IsFractional S I) :
    ∀ n : ℕ, IsFractional S (I ^ n : Submodule R P)
  | 0 => isFractional_of_le_one _ (pow_zero _).le
  | n + 1 => (pow_succ I n).symm ▸ (IsFractional.pow h n).mul h

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