Theorems · Definition · ring theory

MonoidAlgebra.toAdditiveBialgEquiv

(R : Type u_1) →
  (A : Type u_3) →
    (M : Type u_8) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Bialgebra R A] → [inst_3 : Monoid M] → MonoidAlgebra A M ≃ₐc[R] AddMonoidAlgebra A (Additive M)

The bialgebra equivalence between MonoidAlgebra and AddMonoidAlgebra in terms of Additive.

Defined in: Mathlib.RingTheory.Bialgebra.MonoidAlgebra
Cited by: 3 results in Mathlib
Foundations: Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring Semiring Bialgebra Monoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites10

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
CommSemiringstatement and proof · cited by 10,911
Monoidstatement and proof · cited by 3,887
AddMonoidAlgebrastatement · cited by 649
MonoidAlgebrastatement · cited by 590
Additivestatement · cited by 356
Bialgebrastatement and proof · cited by 160
BialgEquivstatement · cited by 88
MonoidAlgebra.toAdditiveAlgEquivproof · cited by 5
BialgEquiv.ofAlgEquivproof · cited by 3

Cited by3

Results whose statement or proof uses this declaration.

MonoidAlgebra.toAdditiveBialgEquiv_singlestatement · cited by 0
MonoidAlgebra.coeff_toAdditiveBialgEquiv_applystatement and proof · cited by 0
MonoidAlgebra.coeff_toAdditiveBialgEquiv_symm_applystatement and proof · cited by 0