Commit 2026-08-25 11:58 2d94cd3b

View on Github →

chore: topologicalGroup -> isTopologicalGroup in names (#43027)

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean

Modified Mathlib/Analysis/Distribution/ContDiffMapSupportedIn.lean

Modified Mathlib/Analysis/Distribution/TestFunction.lean

Modified Mathlib/Analysis/LocallyConvex/WeakDual.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

added theorem WithSeminorms.isTopologicalAddGroup

deleted theorem WithSeminorms.topologicalAddGroup

Modified Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

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

added theorem isTopologicalGroup_iInf

added theorem isTopologicalGroup_induced

added theorem isTopologicalGroup_inf

added theorem isTopologicalGroup_sInf

deleted theorem topologicalGroup_iInf

deleted theorem topologicalGroup_induced

deleted theorem topologicalGroup_inf

deleted theorem topologicalGroup_sInf

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

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

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

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

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

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

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

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

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

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

added theorem IsModuleTopology.isTopologicalAddGroup

deleted theorem IsModuleTopology.topologicalAddGroup

Modified Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean

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

Modified Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean

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

added theorem IsTopologicalRing.isTopologicalAddGroup

deleted theorem IsTopologicalRing.to_topologicalAddGroup

Modified Mathlib/Topology/Instances/Matrix.lean