span_gcd

Mathlib.RingTheory.PrincipalIdealDomain

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

English

The ideal generated by gcd(x,y) equals the ideal generated by x and y.

Русский

Идеал, порождаемый НОД(x,y), равен идеалу, порождаемому x и y.

LaTeX

$$$\mathrm{span}\{\gcd(x,y)\} = \mathrm{span}\{x,y\}$$$

Lean4

theorem span_gcd (x y : R) : span {gcd x y} = span { x, y } := by
  rw [← IsBezout.span_gcd, IsBezout.span_gcd_eq_span_gcd]

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

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

Разделы

Аффилиация

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