Commit 2021-08-17 18:30 90fc0641

chore(algebra/associated): use more dot notation (#8556) I was getting annoyed that working with definitions such as irreducible, prime and associated, I had to write quite verbose terms like dvd_symm_of_irreducible (irreducible_of_prime (prime_of_factor _ hp)) (irreducible_of_prime (prime_of_factor _ hq)) hdvd, where a lot of redundancy can be eliminated with dot notation: (prime_of_factor _ hp).irreducible.dvd_symm (prime_of_factor _ hq).irreducible hdvd. This PR changes the spelling of many of the lemmas in algebra/associated.lean to make usage of dot notation easier. It also adds a few shortcut lemmas that address common patterns. Since this change touches a lot of files, I'll add a RFC label / open a thread on Zulip to see what everyone thinks. Renamings:

• irreducible_of_prime → prime.irreducible
• dvd_symm_of_irreducible → irreducible.dvd_symm
• dvd_symm_iff_of_irreducible → irreducible.dvd_comm (cf. eq.symm versus eq_comm)
• associated_mul_mul → associated.mul_mul
• associated_pow_pow → associated.pow_pow
• dvd_of_associated → associated.dvd
• dvd_dvd_of_associated → associated.dvd_dvd
• dvd_iff_dvd_of_rel_{left,right} → associated.dvd_iff_dvd_{left,right}
• {eq,ne}_zero_iff_of_associated → associated.{eq,ne}_zero_iff
• {irreducible,prime}_of_associated → associated.{irreducible,prime}
• {irreducible,is_unit,prime}_iff_of_associated → associated.{irreducible,is_unit,prime}_iff
• associated_of_{irreducible,prime}_of_dvd → {irreducible,prime}.associated_of_dvd
• gcd_eq_of_associated_{left,right} → associated.gcd_eq_{left,right}
• {irreducible,prime}_of_degree_eq_one_of_monic → monic.{irreducible,prime}_of_degree_eq_one
• gcd_monoid.prime_of_irreducible → irreducible.prime (since the GCD case is probably the only case we care about for this implication. And we could generalize to Schreier domains if not) Additions:
• associated.is_unit := (associated.is_unit_iff _).mp (to match associated.prime and associated.irreducible)
• associated.mul_left := associated.mul_mul (associated.refl _) _
• associated.mul_right := associated.mul_mul _ (associated.refl _) Other changes:
• associated_normalize, normalize_associated, associates.mk_normalize, normalize_apply, prime_X_sub_C: make their final parameter explicit, since it is only inferrable when trying to apply these lemmas. This change helped to golf a few proofs from tactic mode to term mode.
• slight golfing and style fixes