Commit 2025-08-13 11:43 bbd1ca85

View on Github →

chore(LinearAlgebra/BilinearMap): semi-linearize (#27467) Semi-linearizes llcomp and creates a new definition compr₂ₛₗ for the semi-linear version of compr₂. Original PRs: #27353 (#27310, #24208).

Estimated changes

Modified Mathlib/Algebra/Module/Equiv/Defs.lean

modified theorem LinearEquiv.comp_coe

Modified Mathlib/LinearAlgebra/BilinearMap.lean

added theorem LinearMap.bijective_compr₂ₛₗ_of_equiv

added def LinearMap.compr₂ₛₗ

added theorem LinearMap.compr₂ₛₗ_apply

added theorem LinearMap.injective_compr₂ₛₗ_of_injective

modified def LinearMap.llcomp

modified theorem LinearMap.llcomp_apply'

modified theorem LinearMap.llcomp_apply

added theorem LinearMap.surjective_compr₂ₛₗ_of_equiv

added theorem LinearMap.surjective_compr₂ₛₗ_of_exists_rightInverse