Commit 2023-03-01 18:09 bfb4f1a5

View on Github →

feat: port Algebra.Algebra.Bilinear (#2552)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Algebra/Bilinear.lean

added theorem LinearMap.Algebra.coe_lmul_eq_mul

added def LinearMap.Algebra.lmul

added theorem LinearMap.NonUnitalAlgHom.coe_lmul_eq_mul

added def LinearMap.NonUnitalAlgHom.lmul

added theorem LinearMap.commute_mulLeft_right

added def LinearMap.mul'

added theorem LinearMap.mul'_apply

added def LinearMap.mul

added def LinearMap.mulLeft

added def LinearMap.mulLeftRight

added theorem LinearMap.mulLeftRight_apply

added theorem LinearMap.mulLeft_apply

added theorem LinearMap.mulLeft_eq_zero_iff

added theorem LinearMap.mulLeft_injective

added theorem LinearMap.mulLeft_mul

added theorem LinearMap.mulLeft_one

added theorem LinearMap.mulLeft_toAddMonoid_hom

added theorem LinearMap.mulLeft_zero_eq_zero

added def LinearMap.mulRight

added theorem LinearMap.mulRight_apply

added theorem LinearMap.mulRight_eq_zero_iff

added theorem LinearMap.mulRight_injective

added theorem LinearMap.mulRight_mul

added theorem LinearMap.mulRight_one

added theorem LinearMap.mulRight_toAddMonoid_hom

added theorem LinearMap.mulRight_zero_eq_zero

added theorem LinearMap.mul_apply'

added theorem LinearMap.mul_injective

added theorem LinearMap.pow_mulLeft

added theorem LinearMap.pow_mulRight