Theorems · Theorem · commutative algebra

isUnit_gcd_of_eq_mul_gcd

∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {x y x' y' : α},
  x = gcd x y * x' → y = gcd x y * y' → gcd x y ≠ 0 → IsUnit (gcd x' y')

Defined in

Mathlib.Algebra.GCDMonoid.Basic

Cited by

3 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommMonoidWithZeroGCDMonoid