Commit 2023-12-25 14:38 1edf6ce4

View on Github →

feat(Normed/Group): add Filter.HasBasis.cobounded_of_norm (#9244)

Estimated changes

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

added theorem Filter.HasBasis.cobounded_of_norm'

added theorem Filter.hasBasis_cobounded_norm'

Modified Mathlib/Analysis/NormedSpace/Spectrum.lean