gcd_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem gcd_right (a : α) {b : α} (hb : Squarefree b) : Squarefree (gcd a b) :=
  hb.squarefree_of_dvd (gcd_dvd_right _ _)

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