Commit 2026-08-06 00:12 7492625a

View on Github →

chore(Analysis/Seminorm): generalize various lemmas (#42280)

Estimated changes

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Analysis/Seminorm.lean

Modified Mathlib/Topology/Algebra/FilterBasis.lean

modified def ModuleFilterBasis.ofBases

modified def ModuleFilterBasis.topology'

modified structure ModuleFilterBasis