Theorems · Theorem · commutative algebra

UniqueFactorizationMonoid.induction_on_coprime

∀ {α : Type u_1} [inst : CommMonoidWithZero α] [UniqueFactorizationMonoid α] {P : α → Prop} (a : α),
  P 0 →
    (∀ {x : α}, IsUnit x → P x) →
      (∀ {p : α} (i : ℕ), Prime p → P (p ^ i)) → (∀ {x y : α}, IsRelPrime x y → P x → P y → P (x * y)) → P a

If P holds for 0, units and powers of primes, and P x ∧ P y for coprime x, y implies P (x * y), then P holds on all a : α.

Defined in

Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommMonoidWithZeroUniqueFactorizationMonoid