span_singleton_one — Mathlib

English

In a quotient by an ideal, the span of the image of 1 is the whole module, i.e., the span of 1 maps to the top submodule.

Русский

Образ единицы после модульной факторизации порождает всё пространство, то есть порождающая подпоследовательность равна верхнему подмодулю.

LaTeX

$$$\\operatorname{span}_A\\{1\\} = \\top$$$

Lean4

theorem span_singleton_one (I : Ideal A) [I.IsTwoSided] : Submodule.span A {(1 : A ⧸ I)} = ⊤ := by
  rw [← map_one (mk _), ← Submodule.range_mkQ I, ← Submodule.map_top, ← Ideal.span_singleton_one, Ideal.span,
    Submodule.map_span, Set.image_singleton, Submodule.mkQ_apply, Quotient.mk_eq_mk]

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