Theorems · Theorem · group theory
Rep.toAdditive_symm_apply
∀ {M : Type u_1} {G : Type u_2} [inst : Monoid M] [inst_1 : CommGroup G] [inst_2 : MulDistribMulAction M G]
(a : ↑(Rep.ofMulDistribMulAction M G)), Rep.toAdditive.symm a = a- Defined in
- Mathlib.RepresentationTheory.Rep.Basic
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 48 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- 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
- AddEquiv.symmstatement and proof · cited by 530
- Additivestatement · cited by 356
- MulDistribMulActionstatement and proof · cited by 120
- Rep.ofMulDistribMulActionstatement and proof · cited by 12
- Rep.toAdditivestatement and proof · cited by 4
Cited by2
Results whose statement or proof uses this declaration.
- groupCohomology.norm_ofAlgebraAutOnUnits_eqproof · cited by 1
- groupCohomology.exists_div_of_norm_eq_oneproof · cited by 1