Commit 2025-03-31 11:38 d480c857

View on Github →

chore: rename UniformGroup -> IsUniformGroup and UniformAddGroup -> IsUniformAddGroup (#23345) This is a follow-up to #21472.

Estimated changes

modified theorem Nat.sumByResidueClasses
modified theorem multipliable_mabs_iff
modified theorem tprod_subtype_le
added theorem IsUniformGroup.ext
added theorem IsUniformGroup.ext_iff
added theorem IsUniformGroup.mk'
deleted theorem UniformGroup.ext
deleted theorem UniformGroup.ext_iff
deleted theorem UniformGroup.mk'
added theorem isUniformGroup_iInf
added theorem isUniformGroup_inf
added theorem isUniformGroup_sInf
deleted theorem uniformGroup_iInf
deleted theorem uniformGroup_inf
deleted theorem uniformGroup_of_commGroup
deleted theorem uniformGroup_sInf