Commit 2025-02-24 08:51 15d6896f

View on Github →

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

Estimated changes

Modified Mathlib/LinearAlgebra/Pi.lean

added theorem LinearMap.pi_proj

added theorem LinearMap.pi_proj_comp

modified theorem LinearMap.proj_pi

modified theorem LinearMap.proj_surjective

Modified Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean

added theorem ContinuousLinearMap.pi_proj

added theorem ContinuousLinearMap.pi_proj_comp

modified theorem ContinuousLinearMap.proj_pi