Commit 2023-12-01 20:35 d7ae0ec5

View on Github →

refactor: review normed group structure on ContinuousLinearMap (#8725) Move parts of the proof of "two uniformities are equal" up while generalizing it. Also add a ContinuousConstSMul instance that needs less assumptions than ContinuousSMul.

Estimated changes

Modified Mathlib/Analysis/Normed/Group/Basic.lean

modified def NormedGroup.ofSeparation

Modified Mathlib/Analysis/NormedSpace/CompactOperator.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm.lean

Modified Mathlib/Analysis/Seminorm.lean

deleted theorem Seminorm.ball_smul_closedBall

deleted theorem Seminorm.closedBall_smul_ball

added theorem Seminorm.uniformSpace_eq_of_hasBasis

added theorem Seminorm.uniformity_eq_of_hasBasis

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/Algebra/Module/StrongTopology.lean

added theorem ContinuousLinearMap.strongTopology.continuousConstSMul