Commit 2025-10-21 12:12 c0909886

View on Github →

refactor: generalize LinearMap.toMatrix₂ and Matrix.toLinearMap₂ to sesquilinear forms (#30108) Generalize LinearMap.toMatrix₂ to take a sesquilinear map as input. Create Matrix.toLinearMapₛₗ₂ to generalize Matrix.toLinearMap₂ to sesquilinear maps, while still keeping Matrix.toLinearMap₂ to avoid specifying RingHom.id R in the bilinear case. Only do so for maps which are semilinear in the first coordinate to avoid specifying RingHom.id R for the second homomorphism.

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean

modified theorem LinearMap.toMatrix₂Aux_eq

modified theorem LinearMap.toMatrix₂_apply

added theorem LinearMap.toMatrix₂_symm'

added theorem LinearMap.toMatrix₂_toLinearMapₛₗ₂

added theorem Matrix.toLinearMap₂_apply_basis

added theorem Matrix.toLinearMapₛₗ₂_apply

added theorem Matrix.toLinearMapₛₗ₂_apply_basis

added theorem Matrix.toLinearMapₛₗ₂_symm

added theorem Matrix.toLinearMapₛₗ₂_toMatrix₂