spanSingleton

Mathlib.RingTheory.FractionalIdeal.Operations

URI: https://scilib.ai/kg/mathlib#FractionalIdeal.spanSingleton

English

The canonical embedding of spanSingleton x into the ambient submodule equals the span of x.

Русский

Каноническое вложение spanSingleton x в окружающее подмодуль равно span R {x}.

LaTeX

$$$ \text{coeSpanSingleton} = \text{span R\,\{x\}} $$$

Lean4

/-- `spanSingleton x` is the fractional ideal generated by `x` if `0 ∉ S` -/
def spanSingleton :=
  val_proj @wrapped✝.{}

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

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

Разделы

Аффилиация

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