Theorem SkewMonoidAlgebra.ofFinsupp_injective

Modification history

2024-11-14 11:25
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
feat(SkewMonoidAlgebra): add SkewMonoidAlgebra with irreducible def (#15878) …
Added SkewMonoidAlgebra.ofFinsupp_injectiveView on Github →