nsmul — Mathlib

English

If I is a fractional ideal, then for every n ∈ N, the n-th natural multiple n • I is also a fractional ideal.

Русский

Если I — дробный идеал, то для каждого натурального n число n • I тоже является дробным идеалом.

LaTeX

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

Lean4

theorem _root_.IsFractional.nsmul {I : Submodule R P} :
    ∀ n : ℕ, IsFractional S I → IsFractional S (n • I : Submodule R P)
  | 0, _ => by
    rw [zero_smul]
    convert ((0 : Ideal R) : FractionalIdeal S P).isFractional
    simp
  | n + 1, h => by
    rw [succ_nsmul]
    exact (IsFractional.nsmul n h).sup h

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