Theorem ContinuousLinearMap.mk_id

Modification history

2026-05-20 02:56
Mathlib/Topology/Algebra/Module/LinearMap.lean
feat(Analysis): more `LinearIsometryEquiv` API (#39144) …
Added ContinuousLinearMap.mk_idView on Github →