Mathlib Map

Theorems · Definition · number theory

UpperHalfPlane.coe

UpperHalfPlane → ℂ

Canonical embedding of the upper half-plane into ℂ.

Defined in
Mathlib.Analysis.Complex.UpperHalfPlane.Basic
Cited by
288 results in Mathlib
Foundations
Depth 1 from the axioms, rests on 3 definitions · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

UpperHalfPlane.im · cited by 128UpperHalfPlane.imUpperHalfPlane.re · cited by 63UpperHalfPlane.reUpperHalfPlane.ofComplex · cited by 59UpperHalfPlane.ofComplexModularForm.discriminant · cited by 20ModularForm.discriminantUpperHalfPlane.coe_im_pos · cited by 19UpperHalfPlane.coe_im_posModularGroup.fd · cited by 17ModularGroup.fdDerivative.normalizedDerivOfComplex · cited by 17Derivative.normalizedDeri…EisensteinSeries.eisSummand · cited by 15EisensteinSeries.eisSumma…UpperHalfPlane.denom_ne_zero · cited by 15UpperHalfPlane.denom_ne_z…UpperHalfPlane.ext · cited by 14UpperHalfPlane.extUpperHalfPlane.ofComplex_apply · cited by 14UpperHalfPlane.ofComplex_…ModularGroup.fdo · cited by 13ModularGroup.fdoUpperHalfPlane.coe_specialLinearGroup_apply · cited by 10UpperHalfPlane.coe_specia…UpperHalfPlane.isOpenEmbedding_coe · cited by 10UpperHalfPlane.isOpenEmbe…UpperHalfPlane.mdifferentiableAt_iff · cited by 9UpperHalfPlane.mdifferent…Complex · cited by 5565ComplexUpperHalfPlane · cited by 626UpperHalfPlaneUpperHalfPlane.coeCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by298

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 298.