FinGroupCharZero

📁 Source: Mathlib/RepresentationTheory/FinGroupCharZero.lean

Statistics

Metric	Count
Definitions	0
Theorems instInjectiveOfNeZeroCastCard, instProjectiveOfNeZeroCastCard, simple_iff_char_is_norm_one, simple_iff_end_is_rank_one, instInjective, instProjective	6
Total	6

FDRep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instInjectiveOfNeZeroCastCard 📖	mathematical	—	CategoryTheory.Injective FDRep DivisionRing.toRing Field.toDivisionRing DivInvMonoid.toMonoid Group.toDivInvMonoid instLargeCategory EuclideanDomain.toCommRing Field.toEuclideanDomain	—	CategoryTheory.Functor.injective_of_map_injective instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits instPreservesFiniteLimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGVOfIsNoetherianRing IsSimpleModule.instIsNoetherian instIsSimpleModule Rep.instInjective
instProjectiveOfNeZeroCastCard 📖	mathematical	—	CategoryTheory.Projective FDRep DivisionRing.toRing Field.toDivisionRing DivInvMonoid.toMonoid Group.toDivInvMonoid instLargeCategory EuclideanDomain.toCommRing Field.toEuclideanDomain	—	CategoryTheory.Functor.projective_of_map_projective instFullRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV instFaithfulRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV CategoryTheory.preservesEpimorphisms_of_preservesColimitsOfShape CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits instPreservesFiniteColimitsRepForget₂HomSubtypeFGModuleCatLinearMapIdCarrierObjModuleCatIsFGV Rep.instProjective
simple_iff_char_is_norm_one 📖	mathematical	—	CategoryTheory.Simple FDRep DivisionRing.toRing Field.toDivisionRing DivInvMonoid.toMonoid Group.toDivInvMonoid instLargeCategory EuclideanDomain.toCommRing Field.toEuclideanDomain Action.instHasZeroMorphisms FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Preadditive.fullSubcategory ModuleCat.instPreadditive Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finset.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib character InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.card	—	Fintype.card_eq_nat_card NeZero.charZero Fintype.instNeZeroNatCardOfNonempty One.instNonempty Invertible.congr char_orthonormal one_mul smul_eq_mul mul_invOf_self smul_smul mul_comm scalar_product_char_eq_finrank_equivariant simple_iff_end_is_rank_one Finite.of_fintype invOf_eq_inv inv_mul_cancel_of_invertible Nat.cast_one
simple_iff_end_is_rank_one 📖	mathematical	—	CategoryTheory.Simple FDRep DivisionRing.toRing Field.toDivisionRing DivInvMonoid.toMonoid Group.toDivInvMonoid instLargeCategory EuclideanDomain.toCommRing Field.toEuclideanDomain Action.instHasZeroMorphisms FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Preadditive.fullSubcategory ModuleCat.instPreadditive Module.finrank Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup instPreadditive CategoryTheory.Linear.homModule instLinear	—	CategoryTheory.finrank_endomorphism_simple_eq_one instHasKernels instFiniteDimensionalHom Module.finrank_pos_iff_exists_ne_zero commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors CategoryTheory.Limits.IsZero.eq_zero_of_src CategoryTheory.Limits.isIsoZero_iff_source_target_isZero CategoryTheory.Abelian.hasZeroObject IsSimpleModule.instIsNoetherian instIsSimpleModule CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit instInjectiveOfNeZeroCastCard CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.Injective.comp_factorThru CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Limits.comp_zero CategoryTheory.Abelian.isIso_factorThruImage CategoryTheory.Abelian.image.fac finrank_eq_one_iff_of_nonzero' CategoryTheory.Preadditive.epi_of_cancel_zero CategoryTheory.Linear.smul_comp smul_zero CategoryTheory.epi_comp CategoryTheory.Abelian.instEpiFactorThruImage CategoryTheory.isIso_of_mono_of_epi CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory

Rep

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instInjective 📖	mathematical	—	CategoryTheory.Injective Rep DivisionRing.toRing Field.toDivisionRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.Equivalence.map_injective_iff Module.injective_iff_injective_object Module.injective_of_isSemisimpleRing MonoidAlgebra.Submodule.instIsSemisimpleModule
instProjective 📖	mathematical	—	CategoryTheory.Projective Rep DivisionRing.toRing Field.toDivisionRing DivInvMonoid.toMonoid Group.toDivInvMonoid Action.instCategory ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.Equivalence.map_projective_iff IsProjective.iff_projective UnivLE.small UnivLE.self Module.projective_of_isSemisimpleRing MonoidAlgebra.Submodule.instIsSemisimpleModule

---

← Back to Index