mathlib3
fb987e22 - chore(analysis/seminorm): golf (#18089)

Commit

2 years ago

chore(analysis/seminorm): golf (#18089) A part of this PR is forward-ported as leanprover-community/mathlib4#1429

Author

urkud

Parents