pow_eq_span_pow_set

Mathlib.Algebra.Algebra.Operations

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

English

Powers of a submodule equal the span of the corresponding power-set: M^n = span((M)^n).

Русский

Степени подмодуля равны по определению: M^n = span((M)^n).

LaTeX

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

Lean4

theorem pow_eq_span_pow_set (n : ℕ) : M ^ n = span R ((M : Set A) ^ n) := by rw [← span_pow, span_eq]

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

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

Разделы

Аффилиация

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