Commit 2024-10-31 18:17 9fc8d76e

View on Github →

feat: dividing an element of a euclidean domain by its radical (#18449) For a in a EuclideanDomain, define divRadical a as a / radical a

Estimated changes

Modified Mathlib/RingTheory/Radical.lean

added def EuclideanDomain.divRadical

added theorem EuclideanDomain.divRadical_dvd_self

added theorem EuclideanDomain.divRadical_isUnit

added theorem EuclideanDomain.divRadical_mul

added theorem EuclideanDomain.divRadical_mul_radical

added theorem EuclideanDomain.divRadical_ne_zero

added theorem EuclideanDomain.eq_divRadical

added theorem EuclideanDomain.radical_mul_divRadical

added theorem IsCoprime.divRadical