feat(Analysis/Normed): Class for strict multiplicativity of norm

[loefflerd]

This PR makes the following changes:

• Define a mixin class NormMulClass for norms satisfying ‖a * b‖ = ‖a‖ * ‖b‖, and show that any NormedDivisionRing satisfies it.
• Generalise some of the lemmas we currently have for NormedDivisionRing or NormedField to any normed ring satisfying NormMulClass.
• Some minor cleanup I noticed along the way (e.g. deleting a bunch of unnecessary instances in PadicInt).

---

• depends on: [Merged by Bors] - chore (Analysis/Normed): rename norm_mul to norm_mul_le #22871

[github-actions]

PR summary 9039deeaa3

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Analysis.Normed.Ring.Lemmas	1330	1354	+24 (+1.80%)
Mathlib.Analysis.Normed.Field.Basic	1204	1203	-1 (-0.08%)
Mathlib.Analysis.Asymptotics.Defs	1205	1204	-1 (-0.08%)

Import changes for all files

Files	Import difference
10 files Mathlib.Analysis.Asymptotics.Defs Mathlib.Analysis.Asymptotics.Lemmas Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Field.Ultra Mathlib.Analysis.Normed.Group.NullSubmodule Mathlib.Analysis.Normed.MulAction Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Topology.MetricSpace.CauSeqFilter	-1
3 files Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.NumberTheory.SumTwoSquares Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity	2
4 files Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Analysis.Normed.Field.Instances Mathlib.Topology.Algebra.Polynomial Mathlib.Topology.ContinuousMap.Polynomial	22
Mathlib.Analysis.Meromorphic.Divisor.Basic	23
4 files Mathlib.Analysis.Normed.Ring.InfiniteSum Mathlib.Analysis.Normed.Ring.Lemmas Mathlib.Analysis.NormedSpace.Int Mathlib.Topology.Bornology.BoundedOperation	24

---

Declarations diff

+ Dilation.mulLeft
+ Dilation.mulRight
+ Int.instNormMulClass
+ NormMulClass
+ NormMulClass.induced
+ NormMulClass.isAbsoluteValue_norm
+ NormMulClass.isDomain
+ NormMulClass.toNormOneClass
+ instance (priority := 100) NormedDivisionRing.toNormMulClass [β : NormedDivisionRing α] :
+ instance : NormMulClass ℤ_[p] := ⟨fun x y ↦ by simp [norm_def]⟩
+ instance : NormedSpace 𝕜 C₀(α, β)
+ instance [NonUnitalNormedCommRing E] : NonUnitalNormedCommRing (RestrictScalars 𝕜 𝕜' E) := ‹_›
+ instance [NonUnitalNormedRing E] : NonUnitalNormedRing (RestrictScalars 𝕜 𝕜' E) := ‹_›
+ instance [NonUnitalSeminormedCommRing E] : NonUnitalSeminormedCommRing (RestrictScalars 𝕜 𝕜' E)
+ instance [NonUnitalSeminormedRing E] : NonUnitalSeminormedRing (RestrictScalars 𝕜 𝕜' E) := ‹_›
+ instance [NormedAddCommGroup E] : NormedAddCommGroup (RestrictScalars 𝕜 𝕜' E) := ‹_›
+ instance [NormedCommRing E] : NormedCommRing (RestrictScalars 𝕜 𝕜' E) := ‹_›
+ instance [NormedRing E] : NormedRing (RestrictScalars 𝕜 𝕜' E) := ‹_›
+ instance [SeminormedAddCommGroup E] : SeminormedAddCommGroup (RestrictScalars 𝕜 𝕜' E) := ‹_›
+ instance [SeminormedCommRing E] : SeminormedCommRing (RestrictScalars 𝕜 𝕜' E) := ‹_›
+ instance [SeminormedRing E] : SeminormedRing (RestrictScalars 𝕜 𝕜' E) := ‹_›
+ toNormMulClass
+ toSeminormedRing
+-- norm_mul
- Int.instNormOneClass
- antilipschitzWith_mul_left
- instNormedSpace
- instance (priority := 900) NormedDivisionRing.to_normOneClass : NormOneClass α
- instance : Add ℤ_[p] := (by infer_instance : Add (subring p))
- instance : AddCommGroup ℤ_[p] := (by infer_instance : AddCommGroup (subring p))
- instance : IsDomain ℤ_[p] := Function.Injective.isDomain (subring p).subtype Subtype.coe_injective
- instance : Mul ℤ_[p] := (by infer_instance : Mul (subring p))
- instance : Neg ℤ_[p] := (by infer_instance : Neg (subring p))
- instance : NormOneClass ℤ_[p]
- instance : NormedSpace 𝕜 C₀(α, β) where norm_smul_le k f := (norm_smul_le k f.toBCF :)
- instance : One ℤ_[p] := ⟨⟨1, by norm_num⟩⟩
- instance : Sub ℤ_[p] := (by infer_instance : Sub (subring p))
- instance : Zero ℤ_[p] := (by infer_instance : Zero (subring p))
- instance [I : NonUnitalNormedCommRing E] :
- instance [I : NonUnitalNormedRing E] :
- instance [I : NonUnitalSeminormedCommRing E] :
- instance [I : NonUnitalSeminormedRing E] :
- instance [I : NormedAddCommGroup E] :
- instance [I : NormedCommRing E] :
- instance [I : NormedRing E] :
- instance [I : SeminormedAddCommGroup E] :
- instance [I : SeminormedCommRing E] :
- instance [I : SeminormedRing E] :
- isAbsoluteValue
- isAbsoluteValue_norm
- norm_pow
- toSemiNormedRing

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
2262	1	porting notes

Current commit 9039deeaa3
Reference commit 3d3450d07c

You can run this locally as

./scripts/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).

[eric-wieser]

• Rename the field norm_smul_le of NormedSpace and NormedAlgebra to norm_smul_le', to avoid a naming conflict with the lemma inherited via IsBoundedSMul. [These structure field renames are trivial, but make up most of the diff.]

What's the conflict here? Why does it matter if the field name is the same as a lemma name?

[eric-wieser]

• Rename the field norm_mul of the normed ring classes, which states that ‖a * b‖ ≤ ‖a‖ * ‖b‖, to norm_mul_le, to avoid a naming conflict with the norm_mul of NormMulClass.

Could you split this to its own PR? Independently of whether it clashes, I agree this is a better name.

[loefflerd]

• Rename the field norm_smul_le of NormedSpace and NormedAlgebra to norm_smul_le', to avoid a naming conflict with the lemma inherited via IsBoundedSMul. [These structure field renames are trivial, but make up most of the diff.]

What's the conflict here? Why does it matter if the field name is the same as a lemma name?

If you have NormedSpace open, if you try to apply norm_smul_le you have to specify whether you mean _root_.norm_smul_le or NormedSpace.norm_smul_le (which is annoying since they are both, in fact, asserting exactly the same thing!)

[eric-wieser]

If you have NormedSpace open, if you try to apply norm_smul_le you have to specify whether you mean _root_.norm_smul_le or NormedSpace.norm_smul_le (which is annoying since they are both, in fact, asserting exactly the same thing!)

Then the fix is to put protected before norm_smul_le in NormedSpace

[loefflerd]

If you have NormedSpace open, if you try to apply norm_smul_le you have to specify whether you mean _root_.norm_smul_le or NormedSpace.norm_smul_le (which is annoying since they are both, in fact, asserting exactly the same thing!)

Then the fix is to put protected before norm_smul_le in NormedSpace

Can you protect a structure field, rather than a lemma? I didn't know that was possible. (We seem to have a pretty consistent design pattern where foo' is a structure field and foo the lemma which accesses it.)

[eric-wieser]

Can you protect a structure field, rather than a lemma?

Yes!

We seem to have a pretty consistent design pattern where foo' is a structure field and foo the lemma which accesses it.

Usually the pattern is that foo' is the lemma about some internal implementation detail, like toFun, and foo is the lemma about the spelling using a notation class.

[loefflerd]

Can you protect a structure field, rather than a lemma?

Yes!

We seem to have a pretty consistent design pattern where foo' is a structure field and foo the lemma which accesses it.

Usually the pattern is that foo' is the lemma about some internal implementation detail, like toFun, and foo is the lemma about the spelling using a notation class.

NormedDivisionRing.norm_mul' doesn't seem to fit this. I guess that's because norm_mul (unprimed) was previously used for the inequality, so should we now rename NormedDivisionRing.norm_mul' to NormedDivisionRing.norm_mul?

[loefflerd]

bot fix style

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore (Analysis/Normed): rename norm_mul to norm_mul_le #22871
  By Dependent Issues (🤖). Happy coding!