span_singleton_pow — Mathlib

English

For any s ∈ R and n ∈ ℕ, span{ s }^{n} = span{ s^{n} }. (same content as previous item)

Русский

Для любого s ∈ R и n ∈ ℕ выполняется span{ s }^{n} = span{ s^{n} } (то же, что и выше).

LaTeX

$$$ \\forall s \\in R, \\forall n \\in \\mathbb{N}, \\operatorname{span}\\{s\\}^{n} = \\operatorname{span}\\{s^{n}\\}$$$

Lean4

theorem span_singleton_pow (s : R) (n : ℕ) : span { s } ^ n = (span {s ^ n} : Ideal R) := by
  induction n with
  | zero => simp [Set.singleton_one]
  | succ n ih => simp only [pow_succ, ih, span_singleton_mul_span_singleton]

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