Commit 2025-10-21 15:08 7072112c

View on Github →

feat(SkewMonoidAlgebra): Lifts for skew monoid algebras (#29314) Lemmas about different kinds of "lifts" to SkewMonoidAlgebra - Similar in spirit to the MonoidAlgebra.Lift file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean

Created Mathlib/Algebra/SkewMonoidAlgebra/Lift.lean

added theorem SkewMonoidAlgebra.coeff_equivMapDomain

added def SkewMonoidAlgebra.domCongr

added def SkewMonoidAlgebra.domCongrAlg

added theorem SkewMonoidAlgebra.domCongrAlg_apply

added theorem SkewMonoidAlgebra.domCongrAlg_toAlgHom

added theorem SkewMonoidAlgebra.domCongr_refl

added theorem SkewMonoidAlgebra.domCongr_single

added theorem SkewMonoidAlgebra.domCongr_support

added theorem SkewMonoidAlgebra.domCongr_symm

added def SkewMonoidAlgebra.domLCongr

added def SkewMonoidAlgebra.equivMapDomain

added theorem SkewMonoidAlgebra.equivMapDomain_eq_mapDomain

added theorem SkewMonoidAlgebra.equivMapDomain_refl

added theorem SkewMonoidAlgebra.equivMapDomain_single

added theorem SkewMonoidAlgebra.equivMapDomain_trans

added def SkewMonoidAlgebra.lift

added def SkewMonoidAlgebra.liftNCAlgHom

added theorem SkewMonoidAlgebra.lift_apply'

added theorem SkewMonoidAlgebra.lift_apply

added theorem SkewMonoidAlgebra.lift_def

added theorem SkewMonoidAlgebra.lift_of

added theorem SkewMonoidAlgebra.lift_single

added theorem SkewMonoidAlgebra.lift_symm_apply

added theorem SkewMonoidAlgebra.lift_unique'

added theorem SkewMonoidAlgebra.lift_unique

added def SkewMonoidAlgebra.mapDomainAlgHom

added def SkewMonoidAlgebra.submoduleOfSmulMem

added theorem SkewMonoidAlgebra.toFinsupp_equivMapDomain