Commit 2025-10-07 21:16 1ab7069b

View on Github →

feat: a few lemmata about ℂ (#30305) These are useful for facts about unitary elements in C⋆-algebras.

Estimated changes

Modified Mathlib/Analysis/Complex/Basic.lean

added theorem Complex.subset_slitPlane_iff_of_subset_sphere

Modified Mathlib/Analysis/Complex/Norm.lean

added theorem Complex.normSq_ofReal_add_I_mul_sqrt_one_sub

added theorem Complex.normSq_ofReal_sub_I_mul_sqrt_one_sub

added theorem Complex.norm_sub_one_sq_eqOn_sphere

added theorem Complex.norm_sub_one_sq_eq_of_norm_one

Modified Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean

added theorem Complex.continuousOn_arg