instIsPrincipalSpanSingletonSet

Mathlib.RingTheory.Ideal.Span

URI: https://scilib.ai/kg/mathlib#instIsPrincipalSpanSingletonSet

English

For any semiring R and element x ∈ R, the ideal generated by {x} is principal.

Русский

Для любого полупрямого кольца (полукольца) R и элемента x ∈ R идеал, порожденный {x}, является главным идеалом.

LaTeX

$$$\text{IsPrincipal}(\operatorname{Ideal.span}\{x\})$$$

Lean4

instance {R : Type*} [Semiring R] {x : R} : (Ideal.span { x }).IsPrincipal :=
  ⟨x, rfl⟩

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

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

Разделы

Аффилиация

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