Theorem isConformalMap_id

Modification history

2025-10-13 14:40
Mathlib/Analysis/Normed/Operator/Conformal.lean
refactor: make ContinuousLinearMap.id protected (#30362) …
Modified isConformalMap_idView on Github →
2023-04-25 15:53
Mathlib/Analysis/NormedSpace/ConformalLinearMap.lean
feat: port Analysis.NormedSpace.ConformalLinearMap (#3648)
Added isConformalMap_idView on Github →