Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-21 22:33 d98b8e0e

View on Github →

feat(linear_algebra/bilinear_map): semilinearize bilinear maps (#10373) This PR generalizes most of linear_algebra/bilinear_map to semilinear maps. Along the way, we introduce an instance for module S (E →ₛₗ[σ] F), with σ : R →+* S. This allows us to define "semibilinear" maps of type E →ₛₗ[σ] F →ₛₗ[ρ] G, where E, F and G are modules over R₁, R₂ and R₃ respectively, and σ : R₁ →+* R₃ and ρ : R₂ →+* R₃. See mk₂'ₛₗ to see how to construct such a map.

Estimated changes

modified theorem linear_map.coe_smul
modified theorem linear_map.comp_smul
modified theorem linear_map.smul_apply
modified theorem linear_map.smul_comp
modified def linear_map.compl₂
modified theorem linear_map.compl₂_apply
modified def linear_map.compr₂
modified theorem linear_map.compr₂_apply
modified theorem linear_map.ext₂
modified def linear_map.flip
modified theorem linear_map.flip_apply
modified theorem linear_map.flip_inj
modified def linear_map.lcomp
modified theorem linear_map.lcomp_apply
modified def linear_map.lflip
modified def linear_map.llcomp
modified theorem linear_map.llcomp_apply
modified theorem linear_map.map_add₂
modified theorem linear_map.map_neg₂
modified theorem linear_map.map_smul₂
modified theorem linear_map.map_sub₂
modified theorem linear_map.map_sum₂
modified theorem linear_map.map_zero₂
modified def linear_map.mk₂'
modified def linear_map.mk₂