Theorems · Theorem · commutative algebra
WfDvdMonoid.induction_on_irreducible
∀ {α : Type u_1} [inst : CommMonoidWithZero α] [WfDvdMonoid α] {motive : α → Prop} (a : α),
motive 0 →
(∀ (u : α), IsUnit u → motive u) → (∀ (a i : α), a ≠ 0 → Irreducible i → motive a → motive (i * a)) → motive a- Cited by
- 5 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- mul_commproof · cited by 2,262
- IsUnitstatement and proof · cited by 1,602
- CommMonoidWithZerostatement and proof · cited by 913
- Irreduciblestatement and proof · cited by 496
- Irreducible.not_isUnitproof · cited by 42
- WfDvdMonoidstatement and proof · cited by 37
- DvdNotUnitproof · cited by 33
- ne_zero_of_dvd_ne_zeroproof · cited by 26
- WfDvdMonoid.exists_irreducible_factorproof · cited by 12
- wellFounded_dvdNotUnitproof · cited by 7
Cited by5
Results whose statement or proof uses this declaration.
- WfDvdMonoid.exists_factorsproof · cited by 5
- UniqueFactorizationMonoid.induction_on_primeproof · cited by 4
- exists_squarefree_dvd_pow_of_ne_zeroproof · cited by 1
- Polynomial.Gal.splits_in_splittingField_of_compproof · cited by 1