Theorem LinearMap.exact_smul_id_smul_top_mkQ

Modification history

2025-06-15 16:47
Mathlib/RingTheory/Regular/Category.lean
feat(RingTheory/IsSMulRegular): categorical constructions for IsSMulRegular (#23935) …
Added LinearMap.exact_smul_id_smul_top_mkQView on Github →