mathlib

d98b8e0e - feat(linear_algebra/bilinear_map): semilinearize bilinear maps (#10373)

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. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>