mathlib3

79de90f7 - feat(algebra/squarefree): x is squarefree iff (x) is radical in `gcd_monoid` (#17002)

feat(algebra/squarefree): x is squarefree iff (x) is radical in `gcd_monoid` (#17002) Define the notions of radical ideals and radical elements. Show that (under minimal assumptions): + an element is radical iff the ideal it generates is radical; + an ideal is radical iff the quotient by the ideal is reduced; + a ring is reduced iff 0 is a radical element. These are useful glues for #16998. The main theorem is `is_radical_iff_squarefree_or_zero`. The "if" direction only requires `cancel_comm_monoid_with_zero` as noted by @erdOne, and the "only if" direction depends on Cauchy induction #15880 (used to prove `is_radical_iff_pow_one_lt`). Since UFDs are GCDs, we use the main theorem to golf `unique_factorization_monoid.dvd_pow_iff_dvd_of_squarefree` whose conclusion essentially says that (x) is radical. Some unnecessary `normalization_monoid` and `nontrivial` assumptions are also removed from *squarefree.lean*. An earlier version of the PR only proved the main theorem for UFDs, and `le_dedup_self` and `normalized_factors_prod_eq` are remnants from that previous attempt; they are not used to prove the main theorem but are definitely useful lemmas to have. - [x] depends on: #15880 Co-authored-by: Shimon Schlessinger <shimonschlessinger@Eitans-MacBook-Air.local> Co-authored-by: Shimonschlessinger <Shimonschlessinger@users.noreply.github.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>