Commit 2026-02-27 09:51 a5a17ebb

View on Github →

feat: classical "decidability" instances on sets and ideals (#33757)

  • Add decidable equality instances for Set X, Submodule R M (which also gives it for Ideal R) and Associates (Ideal R).
  • This allows one to remove such decidability arguments from lemmas.
  • There was one place where we used an explicit decidability argument to compute an explicit fintype-instance to construct the unique element of some type. This is now replaced by giving the element explicitly.

Estimated changes

modified theorem partialSups_eq_sUnion_image
modified theorem Ideal.count_associates_eq'
modified theorem Ideal.count_associates_eq
modified theorem count_associates_factors_eq
modified theorem count_le_of_ideal_ge
modified theorem irreducible_pow_sup
modified theorem sup_eq_prod_inf_factors
deleted def Ideal.equivFinTwo