gcd_eq — Mathlib

English

In a field, the gcd is given by gcd(a,b) = b if a = 0, and gcd(a,b) = a otherwise.

Русский

В поле НОД выполняется так: gcd(a,b) = b, если a = 0; иначе gcd(a,b) = a.

LaTeX

$$$\\gcd(a,b) = \\begin{cases} b, & a = 0 \\\\ a, & a \\neq 0 \\end{cases}$$$

Lean4

@[simp]
protected theorem gcd_eq [DecidableEq K] (a b : K) : EuclideanDomain.gcd a b = if a = 0 then b else a :=
  by
  unfold EuclideanDomain.gcd
  split_ifs <;> simp [*, Field.mod_eq]

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