Theorems · Theorem · group theory
Rep.applyAsHom_apply
∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : CommMonoid G] {A : Rep.{u_1, u, v} k G} (g : G) (x : ↑A),
(Rep.Hom.hom (A.applyAsHom g)) x = (A.ρ g) x- Defined in
- Mathlib.RepresentationTheory.Rep.Basic
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 49 from the axioms · uses propext, Quot.sound
- Assumes
- SemiringCommMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement · cited by 62,936
- RingHom.idstatement · cited by 18,349
- Semiringstatement and proof · cited by 13,802
- LinearMapstatement · cited by 10,215
- CommMonoidstatement and proof · cited by 2,264
- Repstatement and proof · cited by 843
- Rep.Vstatement and proof · cited by 695
- Representationstatement · cited by 396
- Rep.ρstatement · cited by 356
- Representation.IntertwiningMapstatement · cited by 261
- Rep.Hom.homstatement · cited by 190
- Rep.applyAsHomstatement · cited by 20
Cited by1
Results whose statement or proof uses this declaration.
- Rep.FiniteCyclicGroup.leftRegular.range_norm_eq_ker_applyAsHom_subproof · cited by 1