Character

📁 Source: Mathlib/RepresentationTheory/Character.lean

Statistics

Metric	Count
Definitions character	1
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	10
Total	11

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 AddCommGroup.toAddCommMonoid instAddCommGroupCarrierVFGModuleCat instModuleCarrierVFGModuleCat 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 instFiniteDimensionalCarrierVFGModuleCat 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 instAddCommGroupCarrierVFGModuleCat instModuleCarrierVFGModuleCat LinearMap.addCommGroup Ring.toAddCommGroup 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 instFiniteDimensionalCarrierVFGModuleCat 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 instFiniteDimensionalCarrierVFGModuleCat
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 instAddCommGroupCarrierVFGModuleCat instModuleCarrierVFGModuleCat 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 instFiniteDimensionalCarrierVFGModuleCat 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 instFiniteDimensionalCarrierVFGModuleCat 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 instAddCommGroupCarrierVFGModuleCat instModuleCarrierVFGModuleCat	—	map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass LinearMap.trace_one Module.Free.of_divisionRing instFiniteDimensionalCarrierVFGModuleCat
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 instLargeCategory 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 instLargeCategory EuclideanDomain.toCommRing Field.toEuclideanDomain CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Action.instMonoidalCategory FGModuleCat CategoryTheory.ObjectProperty.FullSubcategory.category ModuleCat ModuleCat.moduleCategory ModuleCat.isFG CategoryTheory.ObjectProperty.fullMonoidalSubcategory ModuleCat.monoidalCategory 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 instFiniteDimensionalCarrierVFGModuleCat
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 instLargeCategory DivisionSemiring.toSemiring Semifield.toDivisionSemiring AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup instPreadditive CategoryTheory.Linear.homModule instLinear	—	smulCommClass_self Module.Finite.linearMap Module.Free.of_divisionRing instFiniteDimensionalCarrierVFGModuleCat mul_comm char_linHom average_char_eq_finrank_invariants LinearEquiv.finrank_eq of_ρ'

---

← Back to Index