Theorems · Inductive type · ring theory
Coalgebra
(R : Type u) → (A : Type v) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid A] → [Module R A] → Type (max u v)
A coalgebra over a commutative (semi)ring R is an R-module equipped with a coassociative
comultiplication Δ and a counit ε obeying the left and right counitality laws.
- Defined in
- Mathlib.RingTheory.Coalgebra.Basic
- Cited by
- 112 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 6 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement · cited by 20,661
- AddCommMonoidstatement · cited by 12,281
- CommSemiringstatement · cited by 10,911
Cited by164
Results whose statement or proof uses this declaration.
- IsGroupLikeElemstatement · cited by 39
- CoalgCat.ofstatement and proof · cited by 24
- GroupLikestatement · cited by 19
- GroupLike.valstatement and proof · cited by 16
- IsGroupLikeElem.comul_eq_tmul_selfstatement and proof · cited by 13
- Coalgebra.IsCocommstatement · cited by 11
- IsGroupLikeElem.counit_eq_onestatement and proof · cited by 9
- CoalgEquiv.toCoalgIsostatement and proof · cited by 8
- CoalgCat.ofHomstatement and proof · cited by 7
- Coalgebra.TensorProduct.ridstatement and proof · cited by 6
- Coalgebra.TensorProduct.assocstatement and proof · cited by 5
- Coalgebra.TensorProduct.lidstatement and proof · cited by 5