Theorem LinearMap.equivariantProjection_condition
Modification history
2024-10-15 10:13
Mathlib/RepresentationTheory/Maschke.lean
refactor(Maschke): use `IsUnit` instead of `Invertible` (#17754)
Modified LinearMap.equivariantProjection_conditionView on Github →