Theorem Seminorm.uniformSpace_eq_of_hasBasis

Modification history

2023-12-01 20:35
Mathlib/Analysis/Seminorm.lean
refactor: review normed group structure on `ContinuousLinearMap` (#8725) …
Added Seminorm.uniformSpace_eq_of_hasBasisView on Github →