coe_spanSingleton

Mathlib.RingTheory.FractionalIdeal.Operations

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

English

The coercion of spanSingleton equals the span of singleton x.

Русский

Приведение spanSingleton к подмодулю равно span {x}.

LaTeX

$$$ (\operatorname{spanSingleton} S x).coeToSubmodule = \operatorname{span} R \{x\} $$$

Lean4

@[simp]
theorem coe_spanSingleton (x : P) : (spanSingleton S x : Submodule R P) = span R { x } :=
  by
  rw [spanSingleton]
  rfl

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

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

Разделы

Аффилиация

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