Theorems · Definition · group theory
Rep.V
{k : Type u} → {G : Type v} → [inst : Semiring k] → [inst_1 : Monoid G] → Rep.{w, u, v} k G → Type wthe underlying type of an object in Rep k G
- Defined in
- Mathlib.RepresentationTheory.Rep.Basic
- Cited by
- 695 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 4 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.
Cited by838
Results whose statement or proof uses this declaration.
- Rep.ρstatement · cited by 356
- Rep.Hom.homstatement · cited by 190
- groupHomology.inhomogeneousChainsproof · cited by 90
- groupCohomology.inhomogeneousCochainsproof · cited by 83
- groupCohomology.cocycles₁statement · cited by 57
- groupHomology.cycles₁statement · cited by 56
- groupCohomology.cocycles₂statement · cited by 45
- groupHomology.cycles₂statement · cited by 43
- groupCohomology.cochainsMapproof · cited by 41
- groupHomology.chainsMapproof · cited by 40
- groupCohomology.cochainsIso₁statement and proof · cited by 35
- Rep.Hom.toModuleCatHomstatement · cited by 34
Showing the 200 most cited of 838.