Commit 2024-10-21 16:43 d2c8bedd

View on Github →

chore(Topology/Algebra/SeparationQuotient): split (#18011) The last 50 lines of the file cause massive import increase in downstream files.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

Modified Mathlib/Analysis/Normed/Module/Span.lean

Modified Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean

Modified Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

Modified Mathlib/Analysis/NormedSpace/BallAction.lean

Modified Mathlib/Analysis/NormedSpace/ConformalLinearMap.lean

Modified Mathlib/Analysis/NormedSpace/ENorm.lean

Modified Mathlib/Analysis/NormedSpace/Real.lean

Modified Mathlib/Analysis/NormedSpace/SphereNormEquiv.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

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

Renamed Mathlib/Topology/Algebra/SeparationQuotient.lean to Mathlib/Topology/Algebra/SeparationQuotient/Basic.lean

deleted theorem SeparationQuotient.exists_out_continuousLinearMap

deleted theorem SeparationQuotient.mkCLM_comp_outCLM

deleted theorem SeparationQuotient.mk_comp_outCLM

deleted theorem SeparationQuotient.mk_outCLM

deleted theorem SeparationQuotient.outCLM_embedding

deleted theorem SeparationQuotient.outCLM_injective

deleted theorem SeparationQuotient.outCLM_isUniformEmbedding

deleted theorem SeparationQuotient.outCLM_isUniformInducing

deleted theorem SeparationQuotient.outCLM_uniformContinuous

deleted theorem SeparationQuotient.postcomp_mkCLM_surjective

Created Mathlib/Topology/Algebra/SeparationQuotient/Section.lean

added theorem SeparationQuotient.exists_out_continuousLinearMap

added theorem SeparationQuotient.mkCLM_comp_outCLM

added theorem SeparationQuotient.mk_comp_outCLM

added theorem SeparationQuotient.mk_outCLM

added theorem SeparationQuotient.outCLM_embedding

added theorem SeparationQuotient.outCLM_injective

added theorem SeparationQuotient.outCLM_isUniformEmbedding

added theorem SeparationQuotient.outCLM_isUniformInducing

added theorem SeparationQuotient.outCLM_uniformContinuous

added theorem SeparationQuotient.postcomp_mkCLM_surjective

Modified Mathlib/Topology/MetricSpace/Algebra.lean

Modified Mathlib/Topology/PartitionOfUnity.lean