Commit 2026-03-03 17:54 2ad33a37

View on Github →

feat(Algebra/Group/FiniteSupport): add HasFinite(Mul)Support and API (#34658) This adds predicates Function.HasFiniteMulSupport and Function.HasFiniteSupport that indicate that a function has finite (multiplicative) support, plus API lemmas. Both the definition and the API lemmas are tagged fun_prop, so that one can show side goals requiring the (multiplicative) support of a function to be finite by fun_prop. The new material is split into two files Algebra.Group.FiniteSupport.{Defs|Basic}, to allow for lighter imports when just needing the definitions. Some (not yet conclusive) discussion is here on Zulip: #mathlib4 > fun_prop for finite (multiplicative) support? @ 💬.

Estimated changes

modified theorem MonoidHom.map_finprod
modified theorem finprod_apply
modified theorem finprod_cond_ne
modified theorem finprod_curry
modified theorem finprod_curry₃
modified theorem finprod_def
modified theorem finprod_div_distrib
modified theorem finprod_eq_prod
modified theorem finprod_le_finprod'
modified theorem finprod_mem_dvd
modified theorem finprod_mul_distrib
modified theorem finprod_option
modified theorem finprod_pow
modified theorem mul_finprod_cond_ne
modified theorem prod_finprod_comm
modified theorem tprod_eq_finprod