Commit 2023-04-25 15:53 1d021f53

View on Github →

feat: port Analysis.NormedSpace.ConformalLinearMap (#3648)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/ConformalLinearMap.lean

added theorem IsConformalMap.comp

added theorem IsConformalMap.ne_zero

added theorem IsConformalMap.smul

added def IsConformalMap

added theorem isConformalMap_const_smul

added theorem isConformalMap_id

added theorem isConformalMap_of_subsingleton