span_pair_isPrincipal

Mathlib.RingTheory.PrincipalIdealDomain

URI: https://scilib.ai/kg/mathlib#IsBezout.span_pair_isPrincipal

← MathLib Explorer

English

span {gcd x y} = span {x, y}.

Русский

span gcd = span {x,y}.

LaTeX

$$Ideal.span { gcd x y } = Ideal.span { x, y }$$

Lean4

instance span_pair_isPrincipal [IsBezout R] (x y : R) : (Ideal.span { x, y }).IsPrincipal := by
  classical exact isPrincipal_of_FG (Ideal.span { x, y }) ⟨{ x, y }, by simp⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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