gcd_zero_eq

Mathlib.Algebra.EuclideanDomain.Field

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

English

In a field, gcd(0,b) = b.

Русский

В поле gcd(0,b) = b.

LaTeX

$$$\\gcd(0,b) = b$$$

Lean4

protected theorem gcd_zero_eq [DecidableEq K] (b : K) : EuclideanDomain.gcd 0 b = b := by rw [Field.gcd_eq, if_pos rfl]

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

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

Разделы

Аффилиация

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