Commit 2023-02-14 06:34 d6be0dc8

View on Github →

feat: port LinearAlgebra.Pi (#2250)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Pi.lean

added def LinearEquiv.finTwoArrow

added def LinearEquiv.funUnique

added theorem LinearEquiv.funUnique_apply

added def LinearEquiv.piCongrLeft'

added def LinearEquiv.piCongrLeft

added def LinearEquiv.piCongrRight

added theorem LinearEquiv.piCongrRight_apply

added theorem LinearEquiv.piCongrRight_refl

added theorem LinearEquiv.piCongrRight_symm

added theorem LinearEquiv.piCongrRight_trans

added def LinearEquiv.piFinTwo

added theorem LinearEquiv.piFinTwo_apply

added def LinearEquiv.piOptionEquivProd

added def LinearEquiv.piRing

added theorem LinearEquiv.piRing_apply

added theorem LinearEquiv.piRing_symmApply

added def LinearEquiv.sumArrowLequivProdArrow

added theorem LinearEquiv.sumArrowLequivProdArrow_apply_fst

added theorem LinearEquiv.sumArrowLequivProdArrow_apply_snd

added theorem LinearEquiv.sumArrowLequivProdArrow_symm_apply_inl

added theorem LinearEquiv.sumArrowLequivProdArrow_symm_apply_inr

added theorem LinearMap.apply_single

added theorem LinearMap.coe_proj

added theorem LinearMap.coe_single

added def LinearMap.diag

added def LinearMap.infᵢKerProjEquiv

added theorem LinearMap.infᵢ_ker_proj

added theorem LinearMap.ker_pi

added def LinearMap.lsum

added theorem LinearMap.lsum_apply

added theorem LinearMap.lsum_single

added def LinearMap.pi

added theorem LinearMap.pi_apply

added theorem LinearMap.pi_comp

added theorem LinearMap.pi_eq_zero

added theorem LinearMap.pi_ext'

added theorem LinearMap.pi_ext'_iff

added theorem LinearMap.pi_ext

added theorem LinearMap.pi_ext_iff

added theorem LinearMap.pi_zero

added def LinearMap.proj

added theorem LinearMap.proj_apply

added theorem LinearMap.proj_pi

added def LinearMap.single

added theorem LinearMap.update_apply

added def LinearMap.vecCons

added theorem LinearMap.vecCons_apply

added def LinearMap.vecCons₂

added def LinearMap.vecEmpty

added theorem LinearMap.vecEmpty_apply

added def LinearMap.vecEmpty₂

added theorem Submodule.binfᵢ_comap_proj

added theorem Submodule.coe_pi

added theorem Submodule.infᵢ_comap_proj

added theorem Submodule.le_comap_single_pi

added theorem Submodule.mem_pi

added def Submodule.pi

added theorem Submodule.pi_empty

added theorem Submodule.pi_mono

added theorem Submodule.pi_top

added theorem Submodule.supᵢ_map_single