Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-04-14 15:57
5cc5bd99
View on Github →
feat(Analysis/Normed/Unbundled/RingSeminorm): turn a ring norm into a normed ring (
#23268
)
Estimated changes
Modified
Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean