Theorems · Theorem · commutative algebra
WfDvdMonoid.exists_irreducible_factor
∀ {α : Type u_1} [inst : CommMonoidWithZero α] [WfDvdMonoid α] {a : α}, ¬IsUnit a → a ≠ 0 → ∃ i, Irreducible i ∧ i ∣ a- Cited by
- 12 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.ofPredproof · cited by 6,101
- IsUnitstatement and proof · cited by 1,602
- CommMonoidWithZerostatement and proof · cited by 913
- Irreduciblestatement and proof · cited by 496
- dvd_rflproof · cited by 80
- of_not_notproof · cited by 51
- dvd_transproof · cited by 50
- WfDvdMonoidstatement and proof · cited by 37
- DvdNotUnitproof · cited by 33
- ne_zero_of_dvd_ne_zeroproof · cited by 26
- WellFounded.has_minproof · cited by 26
- wellFounded_dvdNotUnitproof · cited by 7
Cited by12
Results whose statement or proof uses this declaration.
- WfDvdMonoid.induction_on_irreducibleproof · cited by 5
- UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactorsproof · cited by 3
- Polynomial.exists_monic_irreducible_factorproof · cited by 3
- X_pow_sub_C_irreducible_of_primeproof · cited by 2
- WfDvdMonoid.isRelPrime_of_no_irreducible_factorsproof · cited by 2
- UniqueFactorizationMonoid.exists_mem_normalizedFactorsproof · cited by 2
- Polynomial.factor_dvd_of_not_isUnitproof · cited by 2
- UniqueFactorizationMonoid.exists_mem_factorsproof · cited by 1
- Polynomial.exists_irreducible_of_degree_posproof · cited by 1
- squarefree_iff_no_irreduciblesproof · cited by 1
- Polynomial.irreducible_compproof · cited by 1
- UniqueFactorizationMonoid.exists_prime_iffproof · cited by 0