Theorem Complex.norm_canonicalFactor_eval_circle_eq_one

Modification history

2026-03-18 18:34
Mathlib/Analysis/Complex/CanonicalDecomposition.lean
feat: introduce canonical factors, a.k.a. "Blaschke factors", as used in complex analysis (#36264) …
Added Complex.norm_canonicalFactor_eval_circle_eq_oneView on Github →