Theorems · Definition · ring theory

Bialgebra.comulAlgHom

(R : Type u) →
  (A : Type v) →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Bialgebra R A] → A →ₐ[R] TensorProduct R A A

comulAlgHom R A is the comultiplication of the R-bialgebra A, as an R-algebra map.

Defined in

Mathlib.RingTheory.Bialgebra.Basic

Cited by

20 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringBialgebra