Theorem Representation.leftRegular_norm_eq_zero_iff

Modification history

2026-07-04 08:56

Mathlib/RepresentationTheory/Basic.lean

refactor(Algebra): make `MonoidAlgebra` into a one-field structure (#38714) …

Modified Representation.leftRegular_norm_eq_zero_iff View on Github →

2025-08-04 22:51

Mathlib/RepresentationTheory/Basic.lean

feat(RepresentationTheory): add the norm map (#27362) …

Added Representation.leftRegular_norm_eq_zero_iff View on Github →