Skip to content

Commit

Permalink
replay: #3604 for MonoidAlgebra (#12646)
Browse files Browse the repository at this point in the history
Weaken a couple of `DistribSMul` to `SMulZero` in `MonoidAlgebra`.

This parallels the analogous assumptions in the `AddMonoidAlgebra` instances that were weakened in #3604.

Found in the context of unifying `AddMonoidAlgebra` and `MonoidAlgebra`.
  • Loading branch information
adomani committed May 4, 2024
1 parent 25b2fcc commit 447d24f
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions Mathlib/Algebra/MonoidAlgebra/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -386,8 +386,8 @@ instance module [Semiring R] [Semiring k] [Module R k] : Module R (MonoidAlgebra
Finsupp.module G k
#align monoid_algebra.module MonoidAlgebra.module

instance faithfulSMul [Monoid R] [Semiring k] [DistribMulAction R k] [FaithfulSMul R k]
[Nonempty G] : FaithfulSMul R (MonoidAlgebra k G) :=
instance faithfulSMul [Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] :
FaithfulSMul R (MonoidAlgebra k G) :=
Finsupp.faithfulSMul
#align monoid_algebra.has_faithful_smul MonoidAlgebra.faithfulSMul

Expand All @@ -396,12 +396,12 @@ instance isScalarTower [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMu
Finsupp.isScalarTower G k
#align monoid_algebra.is_scalar_tower MonoidAlgebra.isScalarTower

instance smulCommClass [Monoid R] [Monoid S] [Semiring k] [DistribMulAction R k]
[DistribMulAction S k] [SMulCommClass R S k] : SMulCommClass R S (MonoidAlgebra k G) :=
instance smulCommClass [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] :
SMulCommClass R S (MonoidAlgebra k G) :=
Finsupp.smulCommClass G k
#align monoid_algebra.smul_comm_tower MonoidAlgebra.smulCommClass

instance isCentralScalar [Monoid R] [Semiring k] [DistribMulAction R k] [DistribMulAction Rᵐᵒᵖ k]
instance isCentralScalar [Semiring k] [SMulZeroClass R k] [SMulZeroClass Rᵐᵒᵖ k]
[IsCentralScalar R k] : IsCentralScalar R (MonoidAlgebra k G) :=
Finsupp.isCentralScalar G k
#align monoid_algebra.is_central_scalar MonoidAlgebra.isCentralScalar
Expand Down

0 comments on commit 447d24f

Please sign in to comment.