Theorems · Definition · group theory
Rep.diagonal
(k : Type u) → (G : Type v) → [inst : Ring k] → [inst_1 : Monoid G] → ℕ → Rep.{max u v, u, v} k GThe k-linear G-representation on k[Gⁿ], induced by left multiplication.
- Defined in
- Mathlib.RepresentationTheory.Rep.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- Monoidstatement and proof · cited by 3,887
- Repstatement · cited by 843
- Rep.ofMulActionproof · cited by 1
Cited by5
Results whose statement or proof uses this declaration.
- Rep.diagonalSuccIsoFreestatement · cited by 1
- Rep.diagonalHomEquivstatement · cited by 0
- Rep.diagonalOneIsoLeftRegularstatement · cited by 0
- Rep.diagonalSuccIsoTensorTrivialstatement · cited by 0
- Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eqstatement and proof · cited by 0