C never zero to B off K

LemmaC never zero#

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

Lean

Formalized as lem_Cf_never_zero.

Sources
Leanlem_Cf_never_zero
Uses 2 · Used by 1
Proof usesC nonzero off K · C nonzero on K
Used byNever zero

LemmaBlaschke diff#

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

Lean

Formalized as bl_num_diff.

Sources
Leanbl_num_diff
Uses 2 · Used by 1
Proof usesPower nonzero · Finite zeros
Used byDisk analytic

LemmaBlaschke nonzero#

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

Lean

Formalized as lem_bl_num_nonzero.

Sources
Leanlem_bl_num_nonzero
Uses 2 · Used by 1
Proof usesPower nonzero · Finite zeros
Used byNever zero

DefinitionBlaschke B#

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

Lean

Formalized as Bf.

Sources
LeanBf
Used by 5
Used byB and C relation · One minus B · Outside zeros · Derivative form · Log sum

LemmaB and C relation#

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

Lean

Formalized as lem_BfCf.

Sources
Leanlem_BfCf
Uses 1 · Used by 1
Proof usesBlaschke B
Used byB off K

LemmaB division#

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

Lean

Formalized as lem_Bf_div.

Sources
Leanlem_Bf_div
Uses 1 · Used by 2
Proof usesFinite zeros
Used byB off K · B product pow

LemmaB product pow#

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

Lean

Formalized as lem_Bf_prodpow.

Sources
Leanlem_Bf_prodpow
Uses 2 · Used by 1
Proof usesB division · Finite zeros
Used byB off K

LemmaB off K#

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

Lean

Formalized as lem_Bf_off_K.

Sources
Leanlem_Bf_off_K
Uses 3 · Used by 1
Proof usesB and C relation · B division · B product pow
Used byB modulus

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.