gcd_left — Mathlib

English

If a is squarefree in a cancellative commutative monoid with zero and gcd exists, then gcd(a,b) is squarefree.

Русский

Если a квадратно свободен вCancelCommMonoidWithZero и существует НОД, то gcd(a,b) квадратно свободен.

LaTeX

$$$\mathrm{Squarefree}(a) \rightarrow \mathrm{Squarefree}(\gcd(a,b))$$$

Lean4

theorem gcd_left {a : α} (b : α) (ha : Squarefree a) : Squarefree (gcd a b) :=
  ha.squarefree_of_dvd (gcd_dvd_left _ _)

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