Theorems · Theorem · group theory
Rep.full_res
∀ {k : Type u} [inst : Semiring k] {G : Type v1} {H : Type v2} [inst_1 : Monoid G] [inst_2 : Monoid H] (f : H →* G),
Function.Surjective ⇑f → (Rep.resFunctor f).Full- Defined in
- Mathlib.RepresentationTheory.Rep.Res
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 55 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites17
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
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functor.objproof · cited by 19,642
- Semiringstatement and proof · cited by 13,802
- Monoidstatement and proof · cited by 3,887
- MonoidHomstatement and proof · cited by 3,629
- LinearMap.extproof · cited by 844
- Repstatement and proof · cited by 843
- Rep.Vproof · cited by 695
- CategoryTheory.Functor.Fullstatement · cited by 341
- Representation.IntertwiningMap.toLinearMapproof · cited by 205
- CategoryTheory.ConcreteCategory.hom_ofHomproof · cited by 205
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.