Commit 2024-04-17 00:57 42466cc7

View on Github →

chore(Associated): add simps, golf (#11435)

New simp tags or simp lemmas

associated_one_iff_isUnit, associated_zero_iff_eq_zero, Associates.mk_eq_one, Associates.mk_dvd_mk, Associates.mk_isRelPrime_iff, Associates.mk_zero, Associates.quot_out_zero, Associates.le_zero, Associates.prime_mk, Associates.irreducible_mk, Associates.mk_dvdNotUnit_mk_iff, Associates.factors_le, Associates.prod_factors

New gcongr tags

Associates.factors_mono, Associates.prod_mono

Change explicit args to implicit

Associates.prime_mk, Associates.irreducible_mk, Associates.one_or_eq_of_le_of_prime

Change typeclass assumptions

  • drop [Nontrivial _] here and there, mostly in cases when a lemma has _ ≠ _ assumption
  • drop all decidability assumptions in Associates.FactorSetMem
  • drop decidability assumptions when they aren't needed to formulate a theorem

Use WithTop API

Use WithTop.some and ⊤ instead of Option.some and none in UniqueFactorizationDomain.

Renames

  • Associates.isPrimal_iff → Associates.isPrimal_mk;
  • Associates.mk_le_mk_iff_dvd_iff → Associates.mk_le_mk_iff_dvd;
  • Associates.factors_0 → Associates.factors_zero;
  • Associates.factors_eq_none_iff_zero → Associates.factors_eq_top_iff_zero

Estimated changes

modified theorem Associated.eq_zero_iff
modified theorem Associates.dvd_of_mk_le_mk
modified theorem Associates.irreducible_mk
deleted theorem Associates.isPrimal_iff
added theorem Associates.isPrimal_mk
modified theorem Associates.mk_dvd_mk
added theorem Associates.mk_eq_one
modified theorem Associates.mk_le_mk_of_dvd
added theorem Associates.mk_zero
modified theorem Associates.prime_mk
modified theorem gcd_one_left'
modified theorem gcd_one_right'
added theorem isUnit_gcd_one_left
added theorem isUnit_gcd_one_right
modified def Associates.bcount
modified def Associates.count
modified theorem Associates.count_reducible
modified theorem Associates.count_some
modified theorem Associates.count_zero
modified theorem Associates.eq_of_eq_counts
deleted theorem Associates.factors_0
modified theorem Associates.factors_le
modified theorem Associates.factors_prod