Theorems · Theorem · commutative algebra

succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul

∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p : M},
  Prime p → ∀ {a b : M} {k l : ℕ}, p ^ k ∣ a → p ^ l ∣ b → p ^ (k + l + 1) ∣ a * b → p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b

Defined in

Mathlib.Algebra.Prime.Lemmas

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroIsCancelMulZero