Commit 2025-07-15 14:02 4940ad6e

View on Github →

feat(Algebra/SkewMonoidAlgebra/Basic): multiplication and algebraic instances (#26933) Previously #22078.

Estimated changes

Modified Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

added theorem SkewMonoidAlgebra.addHom_ext

added def SkewMonoidAlgebra.basisSingleOne

added def SkewMonoidAlgebra.comapDistribMulActionSelf

added def SkewMonoidAlgebra.comapMulAction

added def SkewMonoidAlgebra.comapSMul

added theorem SkewMonoidAlgebra.comapSMul_def

added theorem SkewMonoidAlgebra.comapSMul_single

added theorem SkewMonoidAlgebra.eq_liftNC

added theorem SkewMonoidAlgebra.induction_on'

added theorem SkewMonoidAlgebra.induction_on

added theorem SkewMonoidAlgebra.intCast_def

added def SkewMonoidAlgebra.liftNC

added def SkewMonoidAlgebra.liftNCRingHom

added theorem SkewMonoidAlgebra.liftNC_mul

added theorem SkewMonoidAlgebra.liftNC_one

added theorem SkewMonoidAlgebra.liftNC_single

added def SkewMonoidAlgebra.mapDomain

added theorem SkewMonoidAlgebra.mapDomain_comp

added theorem SkewMonoidAlgebra.mapDomain_id

added theorem SkewMonoidAlgebra.mapDomain_single

added theorem SkewMonoidAlgebra.mapDomain_smul

added theorem SkewMonoidAlgebra.mul_def

added theorem SkewMonoidAlgebra.natCast_def

modified theorem SkewMonoidAlgebra.ofFinsupp_eq_zero

added theorem SkewMonoidAlgebra.ofFinsupp_neg

added theorem SkewMonoidAlgebra.ofFinsupp_sub

added theorem SkewMonoidAlgebra.single_nat

added theorem SkewMonoidAlgebra.single_neg

modified theorem SkewMonoidAlgebra.single_one_one

added theorem SkewMonoidAlgebra.sum_mapDomain_index

added theorem SkewMonoidAlgebra.sum_smul_index'

added theorem SkewMonoidAlgebra.sum_smul_index

added def SkewMonoidAlgebra.toFinsuppLinearEquiv

modified theorem SkewMonoidAlgebra.toFinsupp_eq_zero

added theorem SkewMonoidAlgebra.toFinsupp_mapDomain

added theorem SkewMonoidAlgebra.toFinsupp_neg

added theorem SkewMonoidAlgebra.toFinsupp_sub