Theorems · Definition · group theory
Rep.norm
{k : Type u} →
[inst : Semiring k] → {G : Type v} → [inst_1 : Group G] → [Fintype G] → (A : Rep.{w, u, v} k G) → CategoryTheory.End AGiven a representation A of a finite group G, norm A is the representation morphism
A ⟶ A defined by x ↦ ∑ A.ρ g x for g in G.
- Defined in
- Mathlib.RepresentationTheory.Rep.Basic
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
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.
- Semiringstatement and proof · cited by 13,802
- Fintypestatement and proof · cited by 7,736
- Groupstatement and proof · cited by 6,238
- Repstatement and proof · cited by 843
- Rep.ρproof · cited by 356
- CategoryTheory.Endstatement · cited by 169
- Rep.ofHomproof · cited by 45
- Representation.normproof · cited by 22
Cited by29
Results whose statement or proof uses this declaration.
- Rep.tateNormproof · cited by 5
- Rep.FiniteCyclicGroup.normHomCompSubproof · cited by 4
- Rep.FiniteCyclicGroup.subCompNormHomproof · cited by 4
- Rep.FiniteCyclicGroup.groupCohomologyπOddstatement · cited by 3
- Rep.FiniteCyclicGroup.groupCohomologyπOdd_eq_zero_iffstatement and proof · cited by 2
- Rep.norm_commstatement · cited by 2
- Rep.norm_comp_d_eq_zerostatement and proof · cited by 2
- Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_normstatement · cited by 1
- Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_substatement and proof · cited by 1
- Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iffstatement and proof · cited by 1
- Rep.normNatTransproof · cited by 1
- Rep.norm_comp_d_eq_zero_assocstatement and proof · cited by 1