Commit 2024-10-15 10:13 b1339713

View on Github →

refactor(Maschke): use IsUnit instead of Invertible (#17754)

Estimated changes

Modified Mathlib/RepresentationTheory/Maschke.lean

modified theorem LinearMap.conjugate_i

modified theorem LinearMap.equivariantProjection_condition

modified theorem MonoidAlgebra.exists_leftInverse_of_injective