Theorem ContinuousLinearMap.iInf_ker_proj

Modification history

2025-12-27 09:40
Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean
chore(*): restrict operations to `LinearMap`s (#33241) …
Modified ContinuousLinearMap.iInf_ker_projView on Github →
2024-12-19 20:34
Mathlib/Topology/Algebra/Module/Basic.lean
chore(Topology/Algebra/Module): split large file (#20036) …
Modified ContinuousLinearMap.iInf_ker_projView on Github →
2023-05-14 07:05
Mathlib/Topology/Algebra/Module/Basic.lean
chore: Rename to `sSup`/`iSup` (#3938) …
Added ContinuousLinearMap.iInf_ker_projView on Github →