Constant rule to Power multiple

LemmaConstant rule#

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

Lean

Formalized as logDerivconst.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1112

LeanlogDerivconst

Used by 1

Used byDerivative form

LemmaOne minus B#

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

Lean

Formalized as oneBneq0.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1121

LeanoneBneq0

Uses 3 · Used by 1

Proof usesBlaschke B · Disk analytic · B zero

Used byDerivative form

LemmaDerivative form#

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

Lean

Formalized as Lf_deriv_is_logBf_deriv.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1132

LeanLf_deriv_is_logBf_deriv

Uses 3 · Used by 1

Proof usesBlaschke B · Constant rule · One minus B

Used byStep one

LemmaProduct rule#

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

Lean

Formalized as logDerivmul.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1142

LeanlogDerivmul

Used by 1

Used byLog sum

LemmaProduct sum#

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

Lean

Formalized as logDerivprod.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1152

LeanlogDerivprod

Used by 1

Used byProduct sum

LemmaQuotient rule#

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

Lean

Formalized as logDerivdiv.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1161

LeanlogDerivdiv

Used by 1

Used byDifference form

LemmaPower rule#

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

Lean

Formalized as logDerivfunpow.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1170

LeanlogDerivfunpow

Used by 1

Used byPower multiple

LemmaDifference nonzero#

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

Lean

Formalized as z_minus_rho_diff_nonzero.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1180

Leanz_minus_rho_diff_nonzero

Uses 1 · Used by 3

Proof usesZero set

Used byFraction nonzero · Difference form · Diff fraction

LemmaNumerator nonzero#

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

Lean

Formalized as blaschke_num_diff_nonzero.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1192

Leanblaschke_num_diff_nonzero

Used by 3

Used byFraction nonzero · Difference form · Diff fraction

LemmaFraction nonzero#

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

Lean

Formalized as blaschke_frac_diff_nonzero.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1203

Leanblaschke_frac_diff_nonzero

Uses 2 · Used by 2

Proof usesNumerator nonzero · Difference nonzero

Used byPower nonzero · Power multiple

LemmaPower nonzero#

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

Lean

Formalized as blaschke_pow_diff_nonzero.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1213

Leanblaschke_pow_diff_nonzero

Uses 1 · Used by 4

Proof usesFraction nonzero

Used byBlaschke diff · Blaschke nonzero · Product nonzero · Product sum

LemmaProduct nonzero#

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

Lean

Formalized as blaschke_prod_diff_nonzero.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1223

Leanblaschke_prod_diff_nonzero

Uses 2 · Used by 2

Proof usesPower nonzero · Finite zeros

Used byOutside zeros · Log sum

LemmaOutside zeros#

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

Lean

Formalized as f_diff_nonzero_outside_Kf.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1233

Leanf_diff_nonzero_outside_Kf

Uses 1 · Used by 1

Proof usesZero set

Used byOutside zeros

LemmaOutside zeros#

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

Lean

Formalized as Bf_diff_nonzero_outside_Kf.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1243

LeanBf_diff_nonzero_outside_Kf

Uses 3

Proof usesOutside zeros · Product nonzero · Blaschke B

LemmaLog sum#

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

Lean

Formalized as logDeriv_fprod_is_sum.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1254

LeanlogDeriv_fprod_is_sum

Uses 2 · Used by 1

Proof usesProduct rule · Product nonzero

Used byLog sum

LemmaLog sum#

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

Lean

Formalized as logDeriv_Bf_is_sum.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1267

LeanlogDeriv_Bf_is_sum

Uses 2 · Used by 1

Proof usesLog sum · Blaschke B

Used byStep one

LemmaFraction form#

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

Lean

Formalized as logDeriv_def_as_frac.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1278

LeanlogDeriv_def_as_frac

Used by 1

Used byStep one

LemmaStep one#

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

Lean

Formalized as Lf_deriv_step1.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1287

LeanLf_deriv_step1

Uses 3 · Used by 1

Proof usesDerivative form · Log sum · Fraction form

Used byStep two

LemmaProduct sum#

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

Lean

Formalized as logDeriv_prod_is_sum.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1299

LeanlogDeriv_prod_is_sum

Uses 3 · Used by 1

Proof usesProduct sum · Finite zeros · Power nonzero

Used bySum multiple

LemmaPower multiple#

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

Lean

Formalized as logDeriv_power_is_mul.

Sources

• Strong PNT (Math Inc) blueprint: PNT/PNT2_LogDerivative.tex, line 1314

LeanlogDeriv_power_is_mul

Uses 2 · Used by 1

Proof usesPower rule · Fraction nonzero

Used bySum multiple

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.