Theorem Complex.canonicalFactor_ne_zero

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.canonicalFactor_ne_zeroView on Github →