Commit 2025-03-17 07:19 ad61a552

View on Github →

chore: split long file Topology.Algebra.Group.Basic (#23002)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Convex/Strict.lean

Modified Mathlib/Dynamics/Flow.lean

Modified Mathlib/Topology/Algebra/Affine.lean

Modified Mathlib/Topology/Algebra/ClosedSubgroup.lean

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

deleted structure AddGroupTopology

deleted def GroupTopology.coinduced

deleted theorem GroupTopology.coinduced_continuous

deleted theorem GroupTopology.continuous_inv'

deleted theorem GroupTopology.continuous_mul'

deleted theorem GroupTopology.ext'

deleted theorem GroupTopology.toTopologicalSpace_bot

deleted theorem GroupTopology.toTopologicalSpace_iInf

deleted theorem GroupTopology.toTopologicalSpace_inf

deleted theorem GroupTopology.toTopologicalSpace_injective

deleted theorem GroupTopology.toTopologicalSpace_le

deleted theorem GroupTopology.toTopologicalSpace_sInf

deleted theorem GroupTopology.toTopologicalSpace_top

deleted structure GroupTopology

deleted theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group

deleted theorem IsClosed.mul_closure_one_eq

deleted theorem IsClosed.mul_left_of_isCompact

deleted theorem IsClosed.mul_right_of_isCompact

deleted theorem IsClosed.smul_left_of_isCompact

deleted theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_group

deleted theorem IsCompact.mul_closure_one_eq_closure

deleted theorem IsOpen.closure_div

deleted theorem IsOpen.closure_mul

deleted theorem IsOpen.div_closure

deleted theorem IsOpen.div_left

deleted theorem IsOpen.div_right

deleted theorem IsOpen.mul_closure

deleted theorem IsOpen.mul_closure_one_eq

deleted theorem IsOpen.mul_left

deleted theorem IsOpen.mul_right

deleted theorem IsTopologicalGroup.t2Space_iff_one_closed

deleted theorem IsTopologicalGroup.t2Space_of_one_sep

deleted theorem MulAction.isClosedMap_quotient

deleted theorem compl_mul_closure_one_eq

deleted theorem compl_mul_closure_one_eq_iff

deleted theorem eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group

deleted theorem exists_closed_nhds_one_inv_eq_mul_subset

deleted theorem group_inseparable_iff

deleted theorem mul_singleton_mem_nhds

deleted theorem mul_singleton_mem_nhds_of_nhds_one

deleted theorem singleton_mul_mem_nhds

deleted theorem singleton_mul_mem_nhds_of_nhds_one

deleted theorem subset_interior_div

deleted theorem subset_interior_div_left

deleted theorem subset_interior_div_right

deleted theorem subset_interior_mul'

deleted theorem subset_interior_mul

deleted theorem subset_interior_mul_left

deleted theorem subset_interior_mul_right

deleted theorem subset_interior_smul

deleted theorem subset_mul_closure_one

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

Created Mathlib/Topology/Algebra/Group/GroupTopology.lean

added structure AddGroupTopology

added def GroupTopology.coinduced

added theorem GroupTopology.coinduced_continuous

added theorem GroupTopology.continuous_inv'

added theorem GroupTopology.continuous_mul'

added theorem GroupTopology.ext'

added theorem GroupTopology.toTopologicalSpace_bot

added theorem GroupTopology.toTopologicalSpace_iInf

added theorem GroupTopology.toTopologicalSpace_inf

added theorem GroupTopology.toTopologicalSpace_injective

added theorem GroupTopology.toTopologicalSpace_le

added theorem GroupTopology.toTopologicalSpace_sInf

added theorem GroupTopology.toTopologicalSpace_top

added structure GroupTopology

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

Created Mathlib/Topology/Algebra/Group/Pointwise.lean

added theorem HasCompactSupport.eq_zero_or_locallyCompactSpace_of_group

added theorem IsClosed.mul_closure_one_eq

added theorem IsClosed.mul_left_of_isCompact

added theorem IsClosed.mul_right_of_isCompact

added theorem IsClosed.smul_left_of_isCompact

added theorem IsCompact.locallyCompactSpace_of_mem_nhds_of_group

added theorem IsCompact.mul_closure_one_eq_closure

added theorem IsOpen.closure_div

added theorem IsOpen.closure_mul

added theorem IsOpen.div_closure

added theorem IsOpen.div_left

added theorem IsOpen.div_right

added theorem IsOpen.mul_closure

added theorem IsOpen.mul_closure_one_eq

added theorem IsOpen.mul_left

added theorem IsOpen.mul_right

added theorem IsTopologicalGroup.t2Space_iff_one_closed

added theorem IsTopologicalGroup.t2Space_of_one_sep

added theorem MulAction.isClosedMap_quotient

added theorem compl_mul_closure_one_eq

added theorem compl_mul_closure_one_eq_iff

added theorem eq_zero_or_locallyCompactSpace_of_support_subset_isCompact_of_group

added theorem exists_closed_nhds_one_inv_eq_mul_subset

added theorem group_inseparable_iff

added theorem mul_singleton_mem_nhds

added theorem mul_singleton_mem_nhds_of_nhds_one

added theorem singleton_mul_mem_nhds

added theorem singleton_mul_mem_nhds_of_nhds_one

added theorem subset_interior_div

added theorem subset_interior_div_left

added theorem subset_interior_div_right

added theorem subset_interior_mul'

added theorem subset_interior_mul

added theorem subset_interior_mul_left

added theorem subset_interior_mul_right

added theorem subset_interior_smul

added theorem subset_mul_closure_one

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

Modified Mathlib/Topology/Algebra/GroupCompletion.lean

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

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

Modified Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

Modified Mathlib/Topology/Algebra/Order/UpperLower.lean

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

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