Theorem Representation.asAlgebraHom_mem_of_forall_mem

Modification history

2025-03-11 13:02
Mathlib/RepresentationTheory/Submodule.lean
feat: define irreducible root systems / pairings (#22803)
Added Representation.asAlgebraHom_mem_of_forall_memView on Github →