Commit 2024-08-14 13:46 7565a8d7

View on Github →

feat(RingTheory/Radical): Radical of an element in a unique factorization normalization monoid (#14873) For a unique factorization normalization monoid, define a radical of an element as a product of normalized prime factors (without duplication).

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Radical.lean

added def primeFactors

added theorem primeFactors_pow

added def radical

added theorem radical_dvd_self

added theorem radical_eq_of_associated

added theorem radical_mul_unit

added theorem radical_of_prime

added theorem radical_one_eq

added theorem radical_pow

added theorem radical_pow_of_prime

added theorem radical_unit_eq_one

added theorem radical_unit_mul

added theorem radical_zero_eq