gcd_eq_of_ne

Mathlib.Algebra.EuclideanDomain.Field

URI: https://scilib.ai/kg/mathlib#Field.gcd_eq_of_ne

English

If a ≠ 0, then gcd(a,b) = a for all b.

Русский

Если a ≠ 0, то gcd(a,b) = a для любого b.

LaTeX

$$$\\gcd(a,b) = a \\quad\\text{whenever } a \\neq 0$$$

Lean4

protected theorem gcd_eq_of_ne [DecidableEq K] {a : K} (ha : a ≠ 0) (b : K) : EuclideanDomain.gcd a b = a := by
  rw [Field.gcd_eq, if_neg ha]

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

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

Разделы

Аффилиация

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