span_pow

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.span_pow

← MathLib Explorer

English

For any set s, span(s)^n equals span(s^n) for natural powers n.

Русский

Для множества s верно span(s)^n = span(s^n) для любого n ∈ ℕ.

LaTeX

$$$\\operatorname{span} R(s)^n = \\operatorname{span} R(s^n)$$$

Lean4

theorem span_pow (s : Set A) : ∀ n : ℕ, span R s ^ n = span R (s ^ n)
  | 0 => by rw [pow_zero, pow_zero, one_eq_span_one_set]
  | n + 1 => by rw [pow_succ, pow_succ, span_pow s n, span_mul_span]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru