Theorems · Definition · group theory
Rep.ofMulDistribMulAction
(M : Type u_1) →
(G : Type u_2) → [inst : Monoid M] → [inst_1 : CommGroup G] → [MulDistribMulAction M G] → Rep.{u_2, 0, u_1} ℤ MTurns a CommGroup G with a MulDistribMulAction of a monoid M into a
ℤ-linear M-representation on Additive G.
- Defined in
- Mathlib.RepresentationTheory.Rep.Basic
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 46 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- CommGroupstatement and proof · cited by 990
- Repstatement · cited by 843
- MulDistribMulActionstatement and proof · cited by 120
- Rep.ofproof · cited by 57
- Representation.ofMulDistribMulActionproof · cited by 2
Cited by18
Results whose statement or proof uses this declaration.
- Rep.toAdditivestatement and proof · cited by 4
- Rep.ofAlgebraAutOnUnitsproof · cited by 2
- Rep.toAdditive_applystatement and proof · cited by 2
- Rep.toAdditive_symm_applystatement and proof · cited by 2
- groupCohomology.coboundariesOfIsMulCoboundary₁statement · cited by 1
- groupCohomology.norm_ofAlgebraAutOnUnits_eqstatement and proof · cited by 1
- groupCohomology.exists_div_of_norm_eq_oneproof · cited by 1
- groupCohomology.cocyclesOfIsMulCocycle₁statement · cited by 1
- groupCohomology.cocyclesOfIsMulCocycle₂statement · cited by 1
- groupCohomology.cocyclesOfIsMulCocycle₂_coestatement · cited by 0
- groupCohomology.isMulCoboundary₁_of_mem_coboundaries₁statement and proof · cited by 0
- groupCohomology.isMulCoboundary₂_of_mem_coboundaries₂statement and proof · cited by 0