Commit 2025-03-01 00:18 df2382a8

View on Github →

chore: more porting notes (#22387)

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/Bounded.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

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

Modified Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

Modified Mathlib/Analysis/Seminorm.lean

Modified Mathlib/Topology/Algebra/Affine.lean

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

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

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

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

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

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

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

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

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

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

Modified Mathlib/Topology/Algebra/Monoid.lean

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

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

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

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

Modified Mathlib/Topology/Algebra/UniformFilterBasis.lean

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

deleted theorem comm_topologicalGroup_is_uniform

added theorem uniformGroup_of_commGroup

Modified Mathlib/Topology/Algebra/Valued/ValuationTopology.lean

Modified Mathlib/Topology/Bases.lean

Modified Mathlib/Topology/Basic.lean

Modified Mathlib/Topology/ContinuousMap/Algebra.lean

Modified Mathlib/Topology/ContinuousOn.lean

Modified Mathlib/Topology/DiscreteQuotient.lean

Modified Mathlib/Topology/ExtremallyDisconnected.lean

Modified Mathlib/Topology/Gluing.lean

Modified Mathlib/Topology/Homeomorph.lean

Modified Mathlib/Topology/NhdsSet.lean

Modified Mathlib/Topology/Path.lean

Modified Mathlib/Topology/Sheaves/Skyscraper.lean

Modified Mathlib/Topology/UnitInterval.lean

Modified MathlibTest/CategoryTheory/Elementwise.lean