Def DilationEquiv.mulLeft

Modification history

2024-09-05 04:39

Mathlib/Analysis/Normed/Field/Basic.lean

chore: split Analysis.Normed.Field.Basic (#16479)

Modified DilationEquiv.mulLeft View on Github →

2023-11-29 21:38

Mathlib/Analysis/Normed/Field/Basic.lean

refactor: get rid of `comap norm atTop` (#8262)

Added DilationEquiv.mulLeft View on Github →