Theorems · Definition · commutative algebra
UniqueFactorizationMonoid.radical
{M : Type u_1} → [inst : CommMonoidWithZero M] → [NormalizationMonoid M] → [UniqueFactorizationMonoid M] → M → MThe radical of an element a in a unique factorization monoid is the product of
the prime factors of a.
- Defined in
- Mathlib.RingTheory.Radical.Basic
- Cited by
- 64 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finset.prodproof · cited by 2,356
- CommMonoidWithZerostatement and proof · cited by 913
- UniqueFactorizationMonoidstatement and proof · cited by 279
- NormalizationMonoidstatement and proof · cited by 165
- UniqueFactorizationMonoid.primeFactorsproof · cited by 32
Cited by65
Results whose statement or proof uses this declaration.
- EuclideanDomain.divRadicalproof · cited by 12
- Nat.radical_eq_prod_primeFactorsstatement · cited by 7
- UniqueFactorizationMonoid.radical_dvd_selfstatement and proof · cited by 7
- UniqueFactorizationMonoid.radical_zerostatement · cited by 7
- UniqueFactorizationMonoid.radical.congr_simpstatement and proof · cited by 6
- EuclideanDomain.radical_mul_divRadicalstatement and proof · cited by 5
- UniqueFactorizationMonoid.primeFactors_radicalstatement and proof · cited by 5
- UniqueFactorizationMonoid.radical_ne_zerostatement · cited by 5
- UniqueFactorizationMonoid.radical_onestatement · cited by 5
- UniqueFactorizationMonoid.radical_eq_of_associatedstatement and proof · cited by 4
- Int.radical_natAbs_eq_radicalstatement and proof · cited by 3
- UniqueFactorizationMonoid.isRadical_radicalstatement and proof · cited by 3