Def Module.End.toContinuousLinearMap

Modification history

2024-06-26 17:55
Mathlib/Topology/Algebra/Module/FiniteDimension.lean
feat : added `eigenvalues_mem_spectrum_real` and supporting RCLike coercion results (#13838) …
Added Module.End.toContinuousLinearMapView on Github →