Theorems · Theorem · commutative algebra

pow_dvd_of_mul_eq_pow

∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b c d₁ d₂ : α},
  a ≠ 0 → IsUnit (gcd a b) → ∀ {k : ℕ}, a * b = c ^ k → c = d₁ * d₂ → d₁ ∣ a → d₁ ^ k ≠ 0 ∧ d₁ ^ k ∣ a

Defined in

Mathlib.Algebra.GCDMonoid.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroGCDMonoid