Quotient analytic to Complex logarithm

LemmaQuotient analytic#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 644. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_fzzTanal.

Sources
Leanlem_fzzTanal
Uses 2 · Used by 1
Proof usesInverse analytic · Product analytic
Used byRemovable zero

LemmaOn implies within#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 657. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_AnalOntoWithin.

Sources
Leanlem_AnalOntoWithin
Used by 1
Used byLocal to global

LemmaWithin implies on#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 667. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_AnalWithintoOn.

Sources
Leanlem_AnalWithintoOn
Used by 1
Used byWithin gives on

LemmaDisk split#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 678. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_DR0T.

Sources
Leanlem_DR0T
Used by 1
Used byWithin union

LemmaWithin union#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 689. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_analWWWithin.

Sources
Leanlem_analWWWithin
Uses 1 · Used by 1
Proof usesDisk split
Used byWithin gives on

LemmaWithin gives on#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 700. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_analWWithinAtOn.

Sources
Leanlem_analWWithinAtOn
Uses 2 · Used by 1
Proof usesWithin implies on · Within union
Used byLocal to global

LemmaAt to within#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 713. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_AnalAttoWithin.

Sources
Leanlem_AnalAttoWithin
Used by 1
Used byLocal to global

LemmaLocal to global#

The blueprint of Strong PNT (Math Inc) states this lemma at PNT/PNT1_ComplexAnalysis.tex, line 723. The project gives no license, so trough does not reproduce its text.

Lean

Formalized as lem_analAtOnOn.

Sources
Leanlem_analAtOnOn
Uses 3 · Used by 1
Proof usesAt to within · Within gives on · On implies within
Used byRemovable zero

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.