Theorem IsSMulRegular.skewMonoidAlgebra

Modification history

2024-11-14 11:25

Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

feat(SkewMonoidAlgebra): add SkewMonoidAlgebra with irreducible def (#15878) …

Added IsSMulRegular.skewMonoidAlgebra View on Github →