Commit 2022-10-31 12:47 79de90f7

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.

• depends on: #15880