Theorems · Definition · ring theory

MonoidAlgebra.curryAddEquiv

{R : Type u_1} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : Monoid M] → [inst_2 : Monoid N] → MonoidAlgebra R (M × N) ≃+ MonoidAlgebra (MonoidAlgebra R N) M

A product monoid algebra is a nested monoid algebra.

Defined in: Mathlib.Algebra.MonoidAlgebra.Defs
Cited by: 2 results in Mathlib
Foundations: Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semiring Monoid Monoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Semiringstatement and proof · cited by 13,802
Monoidstatement and proof · cited by 3,887
AddEquivstatement · cited by 1,087
MonoidAlgebrastatement · cited by 590
AddEquiv.symmproof · cited by 530
AddEquiv.transproof · cited by 53
Finsupp.mapRange.addEquivproof · cited by 15
MonoidAlgebra.coeffAddEquivproof · cited by 11
Finsupp.curryAddEquivproof · cited by 7

Cited by3

Results whose statement or proof uses this declaration.

MonoidAlgebra.curryRingEquivproof · cited by 3
MonoidAlgebra.curryAddEquiv_singlestatement · cited by 1
MonoidAlgebra.curryAddEquiv_symm_singlestatement · cited by 1