Commit 2023-02-28 06:48 6ec7f93a

View on Github →

feat: port LinearAlgebra.BilinearMap (#2434)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/BilinearMap.lean

added def LinearMap.compl₁₂

added theorem LinearMap.compl₁₂_apply

added theorem LinearMap.compl₁₂_id_id

added theorem LinearMap.compl₁₂_inj

added def LinearMap.compl₂

added theorem LinearMap.compl₂_apply

added theorem LinearMap.compl₂_id

added def LinearMap.compr₂

added theorem LinearMap.compr₂_apply

added theorem LinearMap.congr_fun₂

added def LinearMap.domRestrict₁₂

added theorem LinearMap.domRestrict₁₂_apply

added def LinearMap.domRestrict₂

added theorem LinearMap.domRestrict₂_apply

added theorem LinearMap.ext₂

added def LinearMap.flip

added theorem LinearMap.flip_apply

added theorem LinearMap.flip_flip

added theorem LinearMap.flip_inj

added theorem LinearMap.ker_lsmul

added def LinearMap.lcomp

added theorem LinearMap.lcomp_apply'

added theorem LinearMap.lcomp_apply

added def LinearMap.lcompₛₗ

added theorem LinearMap.lcompₛₗ_apply

added def LinearMap.lflip

added theorem LinearMap.lflip_apply

added def LinearMap.llcomp

added theorem LinearMap.llcomp_apply'

added theorem LinearMap.llcomp_apply

added def LinearMap.lsmul

added theorem LinearMap.lsmul_apply

added theorem LinearMap.lsmul_injective

added theorem LinearMap.map_add₂

added theorem LinearMap.map_neg₂

added theorem LinearMap.map_smul₂

added theorem LinearMap.map_smulₛₗ₂

added theorem LinearMap.map_sub₂

added theorem LinearMap.map_sum₂

added theorem LinearMap.map_zero₂

added def LinearMap.mk₂'

added theorem LinearMap.mk₂'_apply

added def LinearMap.mk₂'ₛₗ

added theorem LinearMap.mk₂'ₛₗ_apply

added def LinearMap.mk₂

added theorem LinearMap.mk₂_apply