Theorem SkewMonoidAlgebra.coeff_single_mul_of_not_exists_mul

Modification history

2025-08-14 21:19
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
feat(SkewMonoidAlgebra): coeff_mul lemmas (#27255) …
Added SkewMonoidAlgebra.coeff_single_mul_of_not_exists_mulView on Github →