Theorems · Definition · ring theory

Coalgebra.Repr.arbitrary

(R : Type u) →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] → [inst_3 : CoalgebraStruct R A] → (a : A) → Coalgebra.Repr R a (A × A)

An arbitrarily chosen representation.

Defined in: Mathlib.RingTheory.Coalgebra.Basic
Cited by: 5 results in Mathlib
Foundations: Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring AddCommMonoid Module CoalgebraStruct

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites5

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

Modulestatement and proof · cited by 20,661
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
CoalgebraStructstatement and proof · cited by 230
Coalgebra.Reprstatement · cited by 25

Cited by5

Results whose statement or proof uses this declaration.

HopfAlgebra.counit_antipodeproof · cited by 1
HopfAlgebra.antipode_comp_mul_comp_commproof · cited by 1
LinearMap.antipode_mul_idproof · cited by 1
LinearMap.id_mul_antipodeproof · cited by 1
Bialgebra.comul_includeRightproof · cited by 0