Commit 2026-10-27 00:37 8000f01d

View on Github →

chore(Algebra): move LinearMap.proj and LinearMap.pi (#45302) This is needed for using LinearMap.proj in IsApply typeclasses to define an abstract FunLike.eval as a linear map.

Estimated changes

added theorem LinearMap.coe_proj
added def LinearMap.const
added theorem LinearMap.const_apply
added def LinearMap.pi
added theorem LinearMap.pi_apply
added theorem LinearMap.pi_comp
added theorem LinearMap.pi_eq_zero
added theorem LinearMap.pi_proj
added theorem LinearMap.pi_proj_comp
added theorem LinearMap.pi_zero
added def LinearMap.proj
added theorem LinearMap.proj_apply
added theorem LinearMap.proj_pi
deleted theorem LinearMap.coe_proj
deleted def LinearMap.const
deleted theorem LinearMap.const_apply
deleted def LinearMap.pi
deleted theorem LinearMap.pi_apply
deleted theorem LinearMap.pi_comp
deleted theorem LinearMap.pi_eq_zero
deleted theorem LinearMap.pi_proj
deleted theorem LinearMap.pi_proj_comp
deleted theorem LinearMap.pi_zero
deleted def LinearMap.proj
deleted theorem LinearMap.proj_apply
deleted theorem LinearMap.proj_pi
deleted theorem LinearMap.proj_surjective