Commit 2026-07-17 23:35 8baa3d09

View on Github →

feat(Analysis): use IsApply for GroupSeminorm (#41560) Also adds instances for AddCommMonoid

Estimated changes

deleted theorem AddGroupSeminorm.coe_smul
deleted theorem GroupNorm.add_apply
deleted theorem GroupNorm.coe_add
deleted theorem GroupSeminorm.add_apply
deleted theorem GroupSeminorm.coe_add
deleted theorem GroupSeminorm.coe_smul
deleted theorem GroupSeminorm.coe_zero
deleted theorem GroupSeminorm.smul_apply
deleted theorem GroupSeminorm.zero_apply