Commit 2023-03-26 07:04 fa5d1a15

View on Github →

feat: port RepresentationTheory.Maschke (#2986)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Module/LinearMap.lean

Modified Mathlib/Algebra/MonoidAlgebra/Basic.lean

Modified Mathlib/Data/Fintype/Card.lean

Created Mathlib/RepresentationTheory/Maschke.lean

added def LinearMap.conjugate

added theorem LinearMap.conjugate_apply

added theorem LinearMap.conjugate_i

added def LinearMap.equivariantProjection

added theorem LinearMap.equivariantProjection_apply

added theorem LinearMap.equivariantProjection_condition

added def LinearMap.sumOfConjugates

added def LinearMap.sumOfConjugatesEquivariant

added theorem LinearMap.sumOfConjugatesEquivariant_apply

added theorem LinearMap.sumOfConjugates_apply

added theorem MonoidAlgebra.Submodule.exists_isCompl

added theorem MonoidAlgebra.exists_leftInverse_of_injective