feat(Analysis): use IsApply for GroupSeminorm

[mcdoll]

Also adds instances for AddCommMonoid

---

[github-actions]

PR summary e28fd68201

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Normed.Group.Seminorm	731	736	+5 (+0.68%)

Import changes for all files

Files	Import difference
44 files Mathlib.Analysis.Asymptotics.Defs Mathlib.Analysis.Calculus.TangentCone.Basic Mathlib.Analysis.Calculus.TangentCone.Defs Mathlib.Analysis.Calculus.TangentCone.Pi Mathlib.Analysis.Calculus.TangentCone.Prod Mathlib.Analysis.Calculus.TangentCone.Real Mathlib.Analysis.Complex.Exponential Mathlib.Analysis.Complex.Norm Mathlib.Analysis.Complex.Order Mathlib.Analysis.Complex.Trigonometric Mathlib.Analysis.Normed.Affine.Simplex Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Field.TransferInstance Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.Analysis.Normed.Group.Basic Mathlib.Analysis.Normed.Group.Bounded Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Analysis.Normed.Group.Constructions Mathlib.Analysis.Normed.Group.Continuity Mathlib.Analysis.Normed.Group.Indicator Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Normed.Group.Real Mathlib.Analysis.Normed.Group.Subgroup Mathlib.Analysis.Normed.Group.Submodule Mathlib.Analysis.Normed.Module.MStructure Mathlib.Analysis.Normed.Order.Basic Mathlib.Analysis.Normed.Order.Hom.Basic Mathlib.Analysis.Normed.Order.Hom.Ultra Mathlib.Analysis.Normed.Ring.Basic Mathlib.Analysis.Normed.Ring.Finite Mathlib.Analysis.Normed.Ring.TransferInstance Mathlib.Analysis.Normed.Ring.WithAbs Mathlib.Analysis.Polynomial.CauchyBound Mathlib.Analysis.SpecialFunctions.Log.ERealExp Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic Mathlib.Analysis.SumOverResidueClass Mathlib.InformationTheory.Hamming Mathlib.RingTheory.MvPowerSeries.GaussNorm Mathlib.RingTheory.Polynomial.GaussNorm Mathlib.RingTheory.PowerSeries.GaussNorm Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Topology.EMetricSpace.VariationOnFromTo Mathlib.Topology.MetricSpace.CauSeqFilter	2
Mathlib.Analysis.Normed.Group.Defs Mathlib.Analysis.Normed.Group.Seminorm	5

---

Declarations diff (regex)

+ instance : AddCommMonoid (AddGroupSeminorm E) := fast_instance% FunLike.addCommMonoid
+ instance : AddCommMonoid (GroupSeminorm E) := fast_instance% FunLike.addCommMonoid
+ instance : IsAddApply (GroupNorm E) E ℝ
+ instance : IsAddApply (GroupSeminorm E) E ℝ
+ instance : IsSMulApply R (AddGroupSeminorm E) E ℝ
+ instance : IsSMulApply R (GroupSeminorm E) E ℝ
+ instance : IsSMulApply R (NonarchAddGroupSeminorm E) E ℝ
+ instance : IsZeroApply (GroupSeminorm E) E ℝ
+ instance : IsZeroApply (NonarchAddGroupSeminorm E) E ℝ
+++--- coe_smul
+++--- smul_apply
+-- coe_zero
+-- zero_apply
-- add_apply
-- coe_add

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit e28fd68).

• +12 new declarations
• −0 removed declarations

+AddGroupNorm.instIsAddApplyReal
+AddGroupSeminorm.instAddCommMonoid
+AddGroupSeminorm.instIsAddApplyReal
+AddGroupSeminorm.instIsSMulApplyReal
+AddGroupSeminorm.instIsZeroApplyReal
+GroupNorm.instIsAddApplyReal
+GroupSeminorm.instAddCommMonoid
+GroupSeminorm.instIsAddApplyReal
+GroupSeminorm.instIsSMulApplyReal
+GroupSeminorm.instIsZeroApplyReal
+NonarchAddGroupSeminorm.instIsSMulApplyReal
+NonarchAddGroupSeminorm.instIsZeroApplyReal

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit e28fd68201
Reference commit 1a783458e3

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).