Theorems · Definition · group theory

Rep.toAdditive

{M : Type u_1} →
  {G : Type u_2} →
    [inst : Monoid M] →
      [inst_1 : CommGroup G] → [inst_2 : MulDistribMulAction M G] → ↑(Rep.ofMulDistribMulAction M G) ≃+ Additive G

Unfolds ofMulDistribMulAction; useful to keep track of additivity.

Defined in: Mathlib.RepresentationTheory.Rep.Basic
Cited by: 4 results in Mathlib
Foundations: Depth 47 from the axioms · uses propext, Quot.sound
Assumes: Monoid CommGroup MulDistribMulAction

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites8

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
AddEquivstatement · cited by 1,087
CommGroupstatement and proof · cited by 990
Rep.Vstatement and proof · cited by 695
Additivestatement · cited by 356
MulDistribMulActionstatement and proof · cited by 120
AddEquiv.reflproof · cited by 34
Rep.ofMulDistribMulActionstatement and proof · cited by 12

Cited by4

Results whose statement or proof uses this declaration.

Rep.toAdditive_applystatement and proof · cited by 2
Rep.toAdditive_symm_applystatement and proof · cited by 2
groupCohomology.norm_ofAlgebraAutOnUnits_eqstatement and proof · cited by 1
groupCohomology.exists_div_of_norm_eq_oneproof · cited by 1