Character

📁 Source: Mathlib/RepresentationTheory/Character.lean

Statistics

Metric	Count
Definitions character, character	2
Theorems average_char_eq_finrank_invariants, char_conj, char_dual, char_iso, char_linHom, char_mul_comm, char_one, char_orthonormal, char_tensor, scalar_product_char_eq_finrank_equivariant, card_inv_mul_sum_char_eq_finrank, card_inv_mul_sum_char_mul_char_eq_finrank, char_conj, char_dual, char_iso, char_linHom, char_mul_comm, char_one, char_orthonormal, char_tensor	20
Total	22

FDRep

Definitions

Name	Category	Theorems
character 📖	CompOp	11 math math: char_tensor, char_conj, char_mul_comm, average_char_eq_finrank_invariants, char_linHom, char_iso, char_one, char_orthonormal, char_dual, scalar_product_char_eq_finrank_equivariant, simple_iff_char_is_norm_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
average_char_eq_finrank_invariants 📖	mathematical	—	Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing AddMonoidWithOne.toNatCast Fintype.card Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ character DivInvMonoid.toMonoid Group.toDivInvMonoid Module.finrank FGModuleCat.carrier CommRing.toRing Action.V FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG Submodule CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants ρ DivisionSemiring.toSemiring Semifield.toDivisionSemiring Submodule.addCommMonoid Submodule.module	—	smulCommClass_self LinearMap.IsProj.trace Representation.isProj_averageMap Module.Free.of_divisionRing FiniteDimensional.finiteDimensional_submodule FGModuleCat.instFiniteCarrier invOf_eq_inv Finset.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass IsScalarTower.left Representation.asAlgebraHom_single one_smul LinearMap.semilinearMapClass SemilinearMapClass.distribMulActionSemiHomClass
char_conj 📖	mathematical	—	character DivInvMonoid.toMonoid Group.toDivInvMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	char_mul_comm inv_mul_cancel_left
char_dual 📖	mathematical	—	character DivInvMonoid.toMonoid Group.toDivInvMonoid of EuclideanDomain.toCommRing Field.toEuclideanDomain Module.Dual FGModuleCat.carrier CommRing.toRing Action.V FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat.isModule LinearMap.addCommGroup LieRing.toAddCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.to_smulCommClass Algebra.id Module.Finite.linearMap Module.Free.of_divisionRing FGModuleCat.instFiniteCarrier Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self Representation.dual ρ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	LinearMap.trace_transpose' Module.Free.of_divisionRing FGModuleCat.instFiniteCarrier
char_iso 📖	mathematical	—	character	—	RingHomInvPair.ids smulCommClass_self Iso.conj_ρ LinearMap.trace_conj'
char_linHom 📖	mathematical	—	character DivInvMonoid.toMonoid Group.toDivInvMonoid of EuclideanDomain.toCommRing Field.toEuclideanDomain LinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring FGModuleCat.carrier CommRing.toRing Action.V FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat.isModule LinearMap.addCommGroup LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Module.Finite.linearMap DivisionRing.toRing Field.toDivisionRing Module.Free.of_divisionRing FGModuleCat.instFiniteCarrier Representation.linHom ρ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smulCommClass_self Module.Finite.linearMap Module.Free.of_divisionRing FGModuleCat.instFiniteCarrier FGModuleCat.instIsMonoidalModuleCatIsFG Algebra.to_smulCommClass Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self char_iso char_tensor Pi.mul_apply char_dual
char_mul_comm 📖	mathematical	—	character MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	smulCommClass_self map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass LinearMap.trace_mul_comm
char_one 📖	mathematical	—	character MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Module.finrank FGModuleCat.carrier CommRing.toRing EuclideanDomain.toCommRing Field.toEuclideanDomain Action.V FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup CategoryTheory.ObjectProperty.FullSubcategory.obj ModuleCat.isModule	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass LinearMap.trace_one Module.Free.of_divisionRing FGModuleCat.instFiniteCarrier
char_orthonormal 📖	mathematical	—	Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing AddMonoidWithOne.toNatCast Fintype.card Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ character DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid CategoryTheory.Iso FDRep Action.instCategory FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	scalar_product_char_eq_finrank_equivariant Nat.cast_one Nat.cast_zero finrank_hom_simple_simple CategoryTheory.Iso.nonempty_iso_symm
char_tensor 📖	mathematical	—	character CategoryTheory.MonoidalCategoryStruct.tensorObj FDRep DivisionRing.toRing Field.toDivisionRing Action.instCategory FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory CategoryTheory.ObjectProperty.fullMonoidalSubcategory ModuleCat.monoidalCategory EuclideanDomain.toCommRing Field.toEuclideanDomain FGModuleCat.instIsMonoidalModuleCatIsFG Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	FGModuleCat.instIsMonoidalModuleCatIsFG smulCommClass_self LinearMap.trace_tensorProduct' Module.Free.of_divisionRing FGModuleCat.instFiniteCarrier
scalar_product_char_eq_finrank_equivariant 📖	mathematical	—	Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id Invertible.invOf Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing AddMonoidWithOne.toNatCast Fintype.card Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ character DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Module.finrank Quiver.Hom FDRep CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Action.instCategory FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG DivisionSemiring.toSemiring Semifield.toDivisionSemiring AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Action.instPreadditive CategoryTheory.Preadditive.fullSubcategory ModuleCat.instPreadditive CategoryTheory.Linear.homModule Action.instLinear CategoryTheory.Linear.fullSubcategory ModuleCat.instLinear	—	smulCommClass_self Module.Finite.linearMap Module.Free.of_divisionRing FGModuleCat.instFiniteCarrier mul_comm char_linHom average_char_eq_finrank_invariants LinearEquiv.finrank_eq of_ρ'

Representation

Definitions

Name	Category	Theorems
character 📖	CompOp	10 math math: char_conj, char_dual, char_iso, card_inv_mul_sum_char_eq_finrank, card_inv_mul_sum_char_mul_char_eq_finrank, char_tensor, char_mul_comm, char_one, char_linHom, char_orthonormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_inv_mul_sum_char_eq_finrank 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.card Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ character DivInvMonoid.toMonoid Group.toDivInvMonoid Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike invariants DivisionSemiring.toSemiring Semifield.toDivisionSemiring Submodule.addCommMonoid Submodule.module	—	Fintype.card_eq_nat_card smulCommClass_self LinearMap.IsProj.trace isProj_averageMap Module.Free.of_divisionRing FiniteDimensional.finiteDimensional_submodule Nat.card_eq_fintype_card Finset.sum_congr invOf_eq_inv map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass IsScalarTower.left asAlgebraHom_single one_smul LinearMap.semilinearMapClass SemilinearMapClass.distribMulActionSemiHomClass
card_inv_mul_sum_char_mul_char_eq_finrank 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.card Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ character DivInvMonoid.toMonoid Group.toDivInvMonoid Group.toDivisionMonoid Module.finrank IntertwiningMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring AddCommGroup.toAddCommMonoid IntertwiningMap.instAddCommMonoid IntertwiningMap.instModule Semifield.toCommSemiring	—	Finset.sum_congr mul_comm smulCommClass_self card_inv_mul_sum_char_eq_finrank Module.Finite.linearMap Module.Free.of_divisionRing LinearEquiv.finrank_eq
char_conj 📖	mathematical	—	character DivInvMonoid.toMonoid Group.toDivInvMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	char_mul_comm inv_mul_cancel_left
char_dual 📖	mathematical	—	character Module.Dual CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid LinearMap.addCommGroup LieRing.toAddCommGroup LieRing.ofAssociativeRing DivisionRing.toRing Field.toDivisionRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring LinearMap.module NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.to_smulCommClass Algebra.id dual InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	LinearMap.trace_transpose' Module.Free.of_divisionRing
char_iso 📖	mathematical	—	character	—	smulCommClass_self RingHomInvPair.ids Equiv.conj_apply_self LinearMap.trace_conj'
char_linHom 📖	mathematical	—	character LinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid DivInvMonoid.toMonoid Group.toDivInvMonoid LinearMap.addCommGroup LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction linHom Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	smulCommClass_self Algebra.to_smulCommClass char_iso char_tensor Module.Finite.linearMap Module.Free.of_divisionRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self Pi.mul_apply char_dual
char_mul_comm 📖	mathematical	—	character MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	smulCommClass_self map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass LinearMap.trace_mul_comm
char_one 📖	mathematical	—	character MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Module.finrank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass LinearMap.trace_one Module.Free.of_divisionRing
char_orthonormal 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Nat.card Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.univ character DivInvMonoid.toMonoid Group.toDivInvMonoid Group.toDivisionMonoid Equiv DivisionSemiring.toSemiring Semifield.toDivisionSemiring AddCommGroup.toAddCommMonoid AddMonoidWithOne.toOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	isEmpty_or_nonempty card_inv_mul_sum_char_mul_char_eq_finrank Module.finrank_eq_zero_of_subsingleton commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing IntertwiningMap.instFiniteOfIsNoetherian isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule IsIrreducible.instSubsingletonIntertwiningMapOfIsEmptyEquiv Nat.cast_zero NeZero.one char_iso IsIrreducible.finrank_intertwiningMap_self Nat.cast_one
char_tensor 📖	mathematical	—	character TensorProduct Semifield.toCommSemiring Field.toSemifield AddCommGroup.toAddCommMonoid TensorProduct.addCommGroup TensorProduct.instModule tprod Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	smulCommClass_self LinearMap.trace_tensorProduct' Module.Free.of_divisionRing

---

← Back to Index