smul_top — Mathlib

English

Let R be a ring and I an ideal. In the quotient module R/I, for any a ∈ R, the submodule a·(R/I) is precisely the span of the coset ā = a + I; i.e., a·⊤ = span_R{ ā }.

Русский

Пусть R — кольцо и I — идеал. В косом модуле R/I для любого a ∈ R подмодуль a·(R/I) равен линейной оболочке косета ā = a + I; то есть a·⊤ = span_R{ ā }.

LaTeX

$$$ (a \cdot \top) = \operatorname{span}_R\{ \overline{a} \} $, where $\overline{a} = \operatorname{Submodule.Quotient.mk} \\ a$.$$

Lean4

theorem smul_top {R : Type*} [CommRing R] (a : R) (I : Ideal R) :
    (a • ⊤ : Submodule R (R ⧸ I)) = Submodule.span R {Submodule.Quotient.mk a} := by
  simp [← Ideal.Quotient.span_singleton_one, Algebra.smul_def, Submodule.smul_span]

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