Theorem Complex.schwarz_aux

Modification history

2026-01-06 22:13

Mathlib/Analysis/Complex/Schwarz.lean

feat(Schwarz): add a version for maps with derivative zero (#33563) …

Modified Complex.schwarz_aux View on Github →

2026-01-03 17:21

Mathlib/Analysis/Complex/Schwarz.lean

feat(Schwarz): generalize domain (#33511) …

Modified Complex.schwarz_aux View on Github →

2023-06-09 16:21

Mathlib/Analysis/Complex/Schwarz.lean

feat: port Analysis.Complex.Schwarz (#4910)

Added Complex.schwarz_aux View on Github →