Documentation Verification Report

Maschke

📁 Source: Mathlib/RepresentationTheory/Maschke.lean

Statistics

Metric	Count
Definitions `conjugate`, `equivariantProjection`, `sumOfConjugates`, `sumOfConjugatesEquivariant`	4
Theorems `conjugate_apply`, `conjugate_i`, `equivariantProjection_apply`, `equivariantProjection_condition`, `sumOfConjugatesEquivariant_apply`, `sumOfConjugates_apply`, `exists_isCompl`, `instIsSemisimpleModule`, `instIsSemisimpleRepresentation`, `instIsSemisimpleRingAddMonoidAlgebra`, `exists_leftInverse_of_injective`	11
Total	15

LinearMap

Definitions

Name	Category	Theorems
`conjugate` 📖	CompOp	5 math math: `sumOfConjugatesEquivariant_apply`, `conjugate_apply`, `sumOfConjugates_apply`, `equivariantProjection_apply`, `conjugate_i`
`equivariantProjection` 📖	CompOp	2 math math: `equivariantProjection_condition`, `equivariantProjection_apply`
`sumOfConjugates` 📖	CompOp	1 math math: `sumOfConjugates_apply`
`sumOfConjugatesEquivariant` 📖	CompOp	1 math math: `sumOfConjugatesEquivariant_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conjugate_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `conjugate` `MonoidAlgebra` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidAlgebra.semiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Module.toDistribMulAction` `MonoidAlgebra.single` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`conjugate_i` 📖	mathematical	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `MonoidAlgebra` `MonoidAlgebra.semiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidAlgebra.nonAssocSemiring` `Monoid.toMulOneClass`	`conjugate`	—	`conjugate_apply` `map_smul` `SemigroupAction.mul_smul` `MonoidAlgebra.single_mul_single` `mul_one` `inv_mul_cancel` `MonoidAlgebra.one_def` `one_smul`
`equivariantProjection_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidAlgebra.semiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `RingHom.id` `MonoidAlgebra.nonAssocSemiring` `Monoid.toMulOneClass` `AddCommGroup.toAddCommMonoid` `instFunLike` `equivariantProjection` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `Ring.inverse` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.card` `Finset.sum` `Finset.univ` `Semiring.toNonAssocSemiring` `conjugate`	—	`Fintype.card_eq_nat_card` `sumOfConjugatesEquivariant_apply`
`equivariantProjection_condition` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `Nat.card` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `MonoidAlgebra` `MonoidAlgebra.semiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidAlgebra.nonAssocSemiring` `Monoid.toMulOneClass`	`equivariantProjection`	—	`equivariantProjection_apply` `Finset.sum_congr` `conjugate_i` `Finset.sum_const` `Finset.card_univ` `Nat.cast_smul_eq_nsmul` `smul_smul` `Fintype.card_eq_nat_card` `Ring.inverse_mul_cancel` `one_smul`
`sumOfConjugatesEquivariant_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidAlgebra.semiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `RingHom.id` `MonoidAlgebra.nonAssocSemiring` `Monoid.toMulOneClass` `AddCommGroup.toAddCommMonoid` `instFunLike` `sumOfConjugatesEquivariant` `Finset.sum` `Finset.univ` `Semiring.toNonAssocSemiring` `conjugate`	—	`sumOfConjugates_apply`
`sumOfConjugates_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `sumOfConjugates` `Finset.sum` `Finset.univ` `conjugate`	—	`sum_apply`

MonoidAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_leftInverse_of_injective` 📖	mathematical	`LinearMap.ker` `MonoidAlgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `semiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddCommGroup.toAddCommMonoid` `RingHom.id` `nonAssocSemiring` `Monoid.toMulOneClass` `Bot.bot` `Submodule` `Submodule.instBot`	`LinearMap.comp` `RingHomCompTriple.ids` `LinearMap.id`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsScalarTower.of_compHom` `LinearMap.IsScalarTower.compatibleSMul` `Submodule.restrictScalars.congr_simp` `RingHomCompTriple.ids` `LinearMap.ext` `LinearMap.equivariantProjection_condition`

MonoidAlgebra.Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isCompl` 📖	mathematical	—	`IsCompl` `Submodule` `MonoidAlgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidAlgebra.semiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	—	`RingHomCompTriple.ids` `MonoidAlgebra.exists_leftInverse_of_injective` `Submodule.ker_subtype` `LinearMap.isCompl_of_proj` `DFunLike.congr_fun`
`instIsSemisimpleModule` 📖	mathematical	—	`IsSemisimpleModule` `MonoidAlgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MonoidAlgebra.ring` `DivisionRing.toRing` `Field.toDivisionRing` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`exists_isCompl`
`instIsSemisimpleRepresentation` 📖	mathematical	—	`Representation.IsSemisimpleRepresentation` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Representation.isSemisimpleRepresentation_iff_isSemisimpleModule_asModule` `instIsSemisimpleModule`
`instIsSemisimpleRingAddMonoidAlgebra` 📖	mathematical	—	`IsSemisimpleRing` `AddMonoidAlgebra` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddMonoidAlgebra.ring` `DivisionRing.toRing` `Field.toDivisionRing` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`RingEquiv.isSemisimpleRing` `instIsSemisimpleModule` `instFiniteMultiplicative` `Nat.card_congr`

---

← Back to Index