Commit 2024-08-23 10:19 05827b12

View on Github →

feat: algebraic operations on SeparationQuotient _ (#12329) I need this to drop [T2Space _] assumptions here and there.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/SeparationQuotient.lean

added theorem SeparationQuotient.exists_out_continuousLinearMap

added def SeparationQuotient.mkCLM

added theorem SeparationQuotient.mkCLM_comp_outCLM

added def SeparationQuotient.mkMonoidHom

added theorem SeparationQuotient.mk_comp_outCLM

added theorem SeparationQuotient.mk_div

added theorem SeparationQuotient.mk_intCast

added theorem SeparationQuotient.mk_inv

added theorem SeparationQuotient.mk_mul

added theorem SeparationQuotient.mk_natCast

added theorem SeparationQuotient.mk_ofNat

added theorem SeparationQuotient.mk_outCLM

added theorem SeparationQuotient.mk_pow

added theorem SeparationQuotient.mk_smul

added theorem SeparationQuotient.mk_zpow

added theorem SeparationQuotient.outCLM_embedding

added theorem SeparationQuotient.outCLM_injective

added theorem SeparationQuotient.outCLM_uniformContinuous

added theorem SeparationQuotient.outCLM_uniformEmbedding

added theorem SeparationQuotient.outCLM_uniformInducing

Modified Mathlib/Topology/Inseparable.lean

added theorem SeparationQuotient.mk_one