Structure NormedSpace.Core

Modification history

2025-03-03 14:53
Mathlib/Analysis/Normed/Module/Basic.lean
chore: bump toolchain to v4.18.0-rc1 (#22500) …
Modified NormedSpace.CoreView on Github →
2024-07-27 16:22
Mathlib/Analysis/Normed/Module/Basic.lean
feat: add `NormedSpace.Core` structure to easily define normed vector spaces (#13424) …
Added NormedSpace.CoreView on Github →