Def Dilation.mulRight

Modification history

2025-03-29 01:26

Mathlib/Analysis/Normed/Ring/Lemmas.lean

feat(Analysis/Normed): generalize lemmas to NormMulClass (#23376) …

Added Dilation.mulRight View on Github →