Commit 2024-04-08 16:29 03e3005a

View on Github →

feat: generalize boundedFilterSubalgebra (#10519) This previously only worked for normed fields, now it works for seminormed algebras. There is no particular motivation for this beyond seeing where NormedSpace is too strong.

Estimated changes

Modified Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean

Modified Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean

modified theorem Filter.BoundedAtFilter.neg

modified theorem Filter.BoundedAtFilter.smul

modified theorem Filter.ZeroAtFilter.smul

modified def Filter.boundedFilterSubalgebra

modified def Filter.boundedFilterSubmodule

modified theorem Filter.const_boundedAtFilter

modified def Filter.zeroAtFilterSubmodule