Theorem Complex.norm_sub_one_sq_eqOn_sphere

Modification history

2025-10-07 21:16
Mathlib/Analysis/Complex/Norm.lean
feat: a few lemmata about `ℂ` (#30305) …
Added Complex.norm_sub_one_sq_eqOn_sphereView on Github →