Commit 2024-10-28 06:12 091df8ec

View on Github →

chore: split Mathlib.Topology.Algebra.UniformGroup (#18311) Another identified by #18156

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Convex/TotallyBounded.lean

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

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

Modified Mathlib/Topology/Algebra/Equicontinuity.lean

Modified Mathlib/Topology/Algebra/GroupCompletion.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Group.lean

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

Modified Mathlib/Topology/Algebra/UniformConvergence.lean

Modified Mathlib/Topology/Algebra/UniformFilterBasis.lean

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

deleted theorem Filter.HasBasis.uniformity_of_nhds_one

deleted theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul

deleted theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul_swapped

deleted theorem Filter.HasBasis.uniformity_of_nhds_one_swapped

deleted theorem MonoidHom.uniformContinuous_of_continuousAt_one

deleted def TopologicalGroup.toUniformSpace

deleted theorem UniformContinuous.const_mul

deleted theorem UniformContinuous.div

deleted theorem UniformContinuous.div_const

deleted theorem UniformContinuous.inv

deleted theorem UniformContinuous.mul

deleted theorem UniformContinuous.mul_const

deleted theorem UniformContinuous.pow_const

deleted theorem UniformContinuous.zpow_const

deleted theorem UniformGroup.ext

deleted theorem UniformGroup.ext_iff

deleted theorem UniformGroup.mk'

deleted theorem UniformGroup.toUniformSpace_eq

deleted theorem UniformGroup.uniformContinuous_iff_open_ker

deleted theorem UniformGroup.uniformity_countably_generated

deleted theorem comm_topologicalGroup_is_uniform

deleted theorem tendsto_div_comap_self

deleted theorem uniformContinuous_div

deleted theorem uniformContinuous_div_const

deleted theorem uniformContinuous_inv

deleted theorem uniformContinuous_monoidHom_of_continuous

deleted theorem uniformContinuous_mul

deleted theorem uniformContinuous_mul_left

deleted theorem uniformContinuous_mul_right

deleted theorem uniformContinuous_of_continuousAt_one

deleted theorem uniformContinuous_of_tendsto_one

deleted theorem uniformContinuous_pow_const

deleted theorem uniformContinuous_zpow_const

deleted theorem uniformGroup_iInf

deleted theorem uniformGroup_inf

deleted theorem uniformGroup_sInf

deleted theorem uniformity_eq_comap_inv_mul_nhds_one

deleted theorem uniformity_eq_comap_inv_mul_nhds_one_swapped

deleted theorem uniformity_eq_comap_nhds_one'

deleted theorem uniformity_eq_comap_nhds_one

deleted theorem uniformity_eq_comap_nhds_one_swapped

deleted theorem uniformity_translate_mul

Created Mathlib/Topology/Algebra/UniformGroup/Defs.lean

added theorem Filter.HasBasis.uniformity_of_nhds_one

added theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul

added theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul_swapped

added theorem Filter.HasBasis.uniformity_of_nhds_one_swapped

added theorem MonoidHom.uniformContinuous_of_continuousAt_one

added def TopologicalGroup.toUniformSpace

added theorem UniformContinuous.const_mul

added theorem UniformContinuous.div

added theorem UniformContinuous.div_const

added theorem UniformContinuous.inv

added theorem UniformContinuous.mul

added theorem UniformContinuous.mul_const

added theorem UniformContinuous.pow_const

added theorem UniformContinuous.zpow_const

added theorem UniformGroup.ext

added theorem UniformGroup.ext_iff

added theorem UniformGroup.mk'

added theorem UniformGroup.toUniformSpace_eq

added theorem UniformGroup.uniformContinuous_iff_open_ker

added theorem UniformGroup.uniformity_countably_generated

added theorem comm_topologicalGroup_is_uniform

added theorem tendsto_div_comap_self

added theorem uniformContinuous_div

added theorem uniformContinuous_div_const

added theorem uniformContinuous_inv

added theorem uniformContinuous_monoidHom_of_continuous

added theorem uniformContinuous_mul

added theorem uniformContinuous_mul_left

added theorem uniformContinuous_mul_right

added theorem uniformContinuous_of_continuousAt_one

added theorem uniformContinuous_of_tendsto_one

added theorem uniformContinuous_pow_const

added theorem uniformContinuous_zpow_const

added theorem uniformGroup_iInf

added theorem uniformGroup_inf

added theorem uniformGroup_sInf

added theorem uniformity_eq_comap_inv_mul_nhds_one

added theorem uniformity_eq_comap_inv_mul_nhds_one_swapped

added theorem uniformity_eq_comap_nhds_one'

added theorem uniformity_eq_comap_nhds_one

added theorem uniformity_eq_comap_nhds_one_swapped

added theorem uniformity_translate_mul

Modified Mathlib/Topology/Algebra/UniformMulAction.lean

Modified Mathlib/Topology/Algebra/UniformRing.lean

Modified Mathlib/Topology/ContinuousMap/Algebra.lean

Modified Mathlib/Topology/Instances/Real.lean

Modified Mathlib/Topology/UniformSpace/Matrix.lean