Theorem Complex.normSq_ofReal_sub_I_mul_sqrt_one_sub

Modification history

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