pow_subset_pow

Mathlib.Algebra.Algebra.Operations

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

English

For all n, the nth power of the underlying set of M is contained in the underlying set of M^n: (↑M)^n ⊆ ↑(M^n).

Русский

Для всех n выполняется вложение (↑M)^n ⊆ ↑(M^n).

LaTeX

$$$ (\uparrow M : Set A)^{n} \subseteq \uparrow (M^{n} : Submodule R A). $$$

Lean4

theorem pow_subset_pow {n : ℕ} : (↑M : Set A) ^ n ⊆ ↑(M ^ n : Submodule R A) :=
  trans AddSubmonoid.pow_subset_pow (le_pow_toAddSubmonoid M)

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

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

Разделы

Аффилиация

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