Def ContinuousLinearEquiv.piRing

Modification history

2023-08-10 19:52

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified ContinuousLinearEquiv.piRing View on Github →

2023-05-20 01:06

Mathlib/Analysis/NormedSpace/FiniteDimension.lean

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

Added ContinuousLinearEquiv.piRing View on Github →