Theorem ContinuousLinearMap.restrict_eq_codRestrict_domRestrict

Modification history

2026-05-20 20:03
Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean
chore: split Topology.Algebra.Module.LinearMap (#39612) …
Modified ContinuousLinearMap.restrict_eq_codRestrict_domRestrictView on Github →
2026-05-15 23:42
Mathlib/Topology/Algebra/Module/LinearMap.lean
feat: ContinuousLinearMap.restrict (#39344)
Added ContinuousLinearMap.restrict_eq_codRestrict_domRestrictView on Github →