Mathlib v3 is deprecated. Go to Mathlib v4

Theorem locally_convex_space.of_basis_zero

Modification history

2022-02-15 12:30

src/topology/algebra/module/locally_convex.lean

feat(topology/algebra/module/locally_convex): define locally convex spaces (#11859)

Added locally_convex_space.of_basis_zero View on Github →