Theorem LinearMap.exact_lsmul_mkQ_smul_top

Modification history

2026-05-10 09:03
Mathlib/RingTheory/Regular/Category.lean
feat(RingTheory): refactor `smulShortComplex` (#37355) …
Added LinearMap.exact_lsmul_mkQ_smul_topView on Github →