Documentation Verification Report

Character

📁 Source: Mathlib/Algebra/Lie/Character.lean

Statistics

Metric	Count
Definitions `LieCharacter`, `lieCharacterEquivLinearDual`	2
Theorems `lieCharacterEquivLinearDual_apply`, `lieCharacterEquivLinearDual_symm_apply`, `lieCharacter_apply_lie`, `lieCharacter_apply_lie'`, `lieCharacter_apply_of_mem_derived`	5
Total	7

LieAlgebra

Definitions

Name	Category	Theorems
`LieCharacter` 📖	CompOp	5 math math: `lieCharacterEquivLinearDual_apply`, `lieCharacterEquivLinearDual_symm_apply`, `lieCharacter_apply_of_mem_derived`, `lieCharacter_apply_lie`, `lieCharacter_apply_lie'`
`lieCharacterEquivLinearDual` 📖	CompOp	2 math math: `lieCharacterEquivLinearDual_apply`, `lieCharacterEquivLinearDual_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lieCharacterEquivLinearDual_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `LieCharacter` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `toModule` `EquivLike.toFunLike` `Equiv.instEquivLike` `lieCharacterEquivLinearDual` `LieHom.toLinearMap` `LieRing.ofAssociativeRing` `CommRing.toRing` `ofAssociativeAlgebra` `Algebra.id`	—	—
`lieCharacterEquivLinearDual_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Module.Dual` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `toModule` `LieCharacter` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `lieCharacterEquivLinearDual` `LieRing.ofAssociativeRing` `CommRing.toRing` `ofAssociativeAlgebra` `Algebra.id`	—	—
`lieCharacter_apply_lie` 📖	mathematical	—	`DFunLike.coe` `LieCharacter` `LieHom.instFunLike` `LieRing.ofAssociativeRing` `CommRing.toRing` `ofAssociativeAlgebra` `Algebra.id` `CommRing.toCommSemiring` `Bracket.bracket` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `lieRingSelfModule` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`LieHom.map_lie` `LieRing.of_associative_ring_bracket` `mul_comm` `sub_self`
`lieCharacter_apply_lie'` 📖	mathematical	—	`Bracket.bracket` `LieRingModule.toBracket` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieRing.toAddCommGroup` `lieRingSelfModule` `DFunLike.coe` `LieCharacter` `LieHom.instFunLike` `ofAssociativeAlgebra` `Algebra.id` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`LieRing.of_associative_ring_bracket` `mul_comm` `sub_self`
`lieCharacter_apply_of_mem_derived` 📖	mathematical	`LieIdeal` `SetLike.instMembership` `LieSubmodule.instSetLike` `LieRing.toAddCommGroup` `toModule` `lieRingSelfModule` `derivedSeries`	`DFunLike.coe` `LieCharacter` `LieHom.instFunLike` `LieRing.ofAssociativeRing` `CommRing.toRing` `ofAssociativeAlgebra` `Algebra.id` `CommRing.toCommSemiring` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Submodule.span_induction` `lieCharacter_apply_lie` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LieHom.instLinearMapClass` `map_add` `SemilinearMapClass.toAddHomClass` `add_zero` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `smul_zero` `LieSubmodule.lieIdeal_oper_eq_linear_span` `lieAlgebraSelfModule` `LieSubmodule.mem_toSubmodule` `derivedSeriesOfIdeal_zero` `derivedSeriesOfIdeal_succ` `derivedSeries_def`

---

← Back to Index