Commit 2026-10-17 10:25 c1e8c680
View on Github →chore: use Type* in a few more places (#44776)
Representation.norm_ofMulDistribMulAction_eq, Matrix.dualNumberEquiv and ValuativeRel.trivialRel (with the lemmas about it) were stated for Type, although the definitions they use work in any universe. This uses Type*.