Theorem ContinuousLinearMap.proj_pi

Modification history

2025-02-24 08:51

Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean

feat(LinearAlgebra/Pi): add `pi_proj` and `pi_proj_comp` (#22162)

Modified ContinuousLinearMap.proj_pi View on Github →

2024-12-19 20:34

Mathlib/Topology/Algebra/Module/Basic.lean

chore(Topology/Algebra/Module): split large file (#20036) …

Modified ContinuousLinearMap.proj_pi View on Github →

2023-04-04 14:45

Mathlib/Topology/Algebra/Module/Basic.lean

feat: port Topology.Algebra.Module.Basic (#2983)

Added ContinuousLinearMap.proj_pi View on Github →