Theorems · Definition · complex analysis
Complex.UnitDisc
Type
The complex unit disc, denoted as 𝔻 within the Complex namespace
- Defined in
- Mathlib.Analysis.Complex.UnitDisc.Basic
- Cited by
- 52 results in Mathlib
- Foundations
- Depth 137 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexproof · cited by 5,565
- Subsemigroup.unitBallproof · cited by 1
Cited by58
Results whose statement or proof uses this declaration.
- Complex.UnitDisc.coestatement · cited by 32
- Complex.UnitDisc.mkstatement · cited by 10
- Complex.UnitDisc.norm_lt_onestatement and proof · cited by 7
- Complex.UnitDisc.imstatement and proof · cited by 5
- Complex.UnitDisc.restatement and proof · cited by 5
- Complex.UnitDisc.isEmbedding_coestatement · cited by 4
- Complex.UnitDisc.coe_injectivestatement · cited by 2
- Complex.UnitDisc.continuous_coestatement · cited by 2
- Complex.UnitDisc.norm_ne_onestatement and proof · cited by 2
- Complex.UnitDisc.casesOnstatement and proof · cited by 1
- Complex.UnitDisc.coe_circle_smulstatement and proof · cited by 1
- Complex.UnitDisc.coe_injstatement and proof · cited by 1