Theorems · Theorem · several complex variables
UpperHalfPlane.contMDiff_denom_zpow
∀ {n : WithTop ℕ∞} (g : GL (Fin 2) ℝ) (k : ℤ),
ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) n fun x => UpperHalfPlane.denom g ↑x ^ k- Cited by
- 2 results in Mathlib
- Foundations
- Depth 287 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Complexstatement and proof · cited by 5,565
- ENatstatement and proof · cited by 4,985
- WithTopstatement and proof · cited by 3,754
- Compl.complproof · cited by 2,925
- modelWithCornersSelfstatement · cited by 920
- UpperHalfPlanestatement and proof · cited by 626
- Matrix.GeneralLinearGroupstatement and proof · cited by 556
- AnalyticAtproof · cited by 321
- UpperHalfPlane.coestatement and proof · cited by 288
- ContMDiffstatement · cited by 278
- UpperHalfPlane.denomstatement and proof · cited by 84
Cited by2
Results whose statement or proof uses this declaration.
- UpperHalfPlane.contMDiff_inv_denomproof · cited by 2
- UpperHalfPlane.mdifferentiable_denom_zpowproof · cited by 0