Theorem FiniteDimensional.complete

Modification history

2024-08-12 18:29

Mathlib/Topology/Algebra/Module/FiniteDimension.lean

chore: move to v4.11.0-rc2 (new `variable` command) (#15726)

Modified FiniteDimensional.complete View on Github →

2023-09-05 10:32

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

feat: generalize some lemmas from a normed space to a TVS (#5771) …

Modified FiniteDimensional.complete View on Github →

2023-05-20 01:06

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

feat: port Analysis.NormedSpace.FiniteDimension (#4123)

Added FiniteDimensional.complete View on Github →