Structures · Algebra
Representation.IsTrivial
A predicate for representations that fix every element.
- Defined in
- Mathlib.RepresentationTheory.Basic
- Shape
- One type argument · adds out
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by24
- groupHomology.H1CoresCoinfOfTrivial
- Representation.isTrivial_def
- Rep.ofQuotient
- Representation.isTrivial_apply
- Representation.ofQuotient
- Rep.desc
- Rep.resOfQuotientIso
- Representation.IsTrivial.out
- groupHomology.H1CoresCoinfOfTrivial_exact
- groupHomology.mapCycles₁_quotientGroupMk'_epi
- groupHomology.H1CoresCoinfOfTrivial_X₃
- Representation.apply_eq_of_coe_eq
- groupHomology.H1CoresCoinfOfTrivial_g
- groupHomology.H1CoresCoinfOfTrivial_g_epi
- Representation.ofQuotient_coe_apply
- Representation.invariants_eq_top
- groupHomology.H1CoresCoinfOfTrivial_X₁
- groupHomology.map₁_quotientGroupMk'_epi
- Rep.instIsTrivialOfOfIsTrivial
- groupHomology.H1CoresCoinfOfTrivial_X₂
- groupHomology.H1CoresCoinfOfTrivial_f
- Rep.desc.congr_simp
- Representation.ofQuotient.congr_simp
- Rep.instIsTrivialVOfCompLinearMapIdρ
Ancestors0
No ancestors.