Theorem LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmul

Modification history

2025-09-15 21:27
Mathlib/Algebra/Algebra/Bilinear.lean
feat(RingTheory/Flat): Add theorems relating Submodule.torsion and Module.Flat (#26783)
Added LinearMap.lift_lsmul_mul_eq_lsmul_lift_lsmulView on Github →