span_singleton_mul_span_singleton

Mathlib.RingTheory.Ideal.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.span_singleton_mul_span_singleton

← MathLib Explorer

English

For any r ∈ R and n ∈ ℕ, span{r}^{n} = span{r^{n}}.

Русский

Пусть r ∈ R и n ∈ ℕ. Тогда span{r}^{n} = span{r^{n}}.

LaTeX

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

Lean4

theorem span_singleton_mul_span_singleton (r s : R) : span { r } * span { s } = (span {r * s} : Ideal R) :=
  by
  unfold span
  rw [Submodule.span_mul_span, Set.singleton_mul_singleton]

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

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

Разделы

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

Аффилиация

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