Zero value to Abs division

LemmaZero value#

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

Lean

Formalized as lem_frho_zero.

Sources

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

Leanlem_frho_zero

Uses 1 · Used by 2

Proof usesZero set

Used byOrder at least one · Zero contrapositive

LemmaZero contrapositive#

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

Lean

Formalized as lem_frho_zero_contra.

Sources

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

Leanlem_frho_zero_contra

Uses 1 · Used by 1

Proof usesZero value

Used byZero excluded

LemmaNot zero#

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

Lean

Formalized as lem_f_is_nonzero.

Sources

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

Leanlem_f_is_nonzero

Used by 1

Used byOrder is integer

LemmaDisk bound#

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

Lean

Formalized as lem_rho_in_disk_R1.

Sources

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

Leanlem_rho_in_disk_R1

Uses 1

Proof usesZero set

LemmaZero excluded#

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

Lean

Formalized as lem_zero_not_in_Kf.

Sources

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

Leanlem_zero_not_in_Kf

Uses 1 · Used by 1

Proof usesZero contrapositive

Used byNonzero rho

LemmaNonzero rho#

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

Lean

Formalized as lem_rho_ne_zero.

Sources

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

Leanlem_rho_ne_zero

Uses 1 · Used by 3

Proof usesZero excluded

Used byRho positive · B zero form · Abs ratio

LemmaMod positive#

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

Lean

Formalized as lem_mod_pos_iff_ne_zero.

Sources

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

Leanlem_mod_pos_iff_ne_zero

Uses 1 · Used by 1

Proof usesAbsolute value positive

Used byRho positive

LemmaRho positive#

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

Lean

Formalized as lem_mod_rho_pos.

Sources

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

Leanlem_mod_rho_pos

Uses 2 · Used by 1

Proof usesNonzero rho · Mod positive

Used byInverse bound

LemmaDisk bound#

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

Lean

Formalized as lem_rho_in_disk_R1_repeat.

Sources

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

Leanlem_rho_in_disk_R1_repeat

Uses 1 · Used by 1

Proof usesZero set

Used byInverse bound

LemmaInverse mono#

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

Lean

Formalized as lem_inv_mono_decr.

Sources

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

Leanlem_inv_mono_decr

Used by 1

Used byInverse bound

LemmaInverse bound#

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

Lean

Formalized as lem_inv_mod_rho_ge_inv_R1.

Sources

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

Leanlem_inv_mod_rho_ge_inv_R1

Uses 3 · Used by 1

Proof usesRho positive · Disk bound · Inverse mono

Used byRatio bound

LemmaMult inequality#

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

Lean

Formalized as lem_mul_pos_preserves_ineq.

Sources

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

Leanlem_mul_pos_preserves_ineq

Used by 1

Used byRatio bound

LemmaRatio bound#

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

Lean

Formalized as lem_R_div_mod_rho_ge_R_div_R1.

Sources

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

Leanlem_R_div_mod_rho_ge_R_div_R1

Uses 2

Proof usesInverse bound · Mult inequality

LemmaMod product#

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

Lean

Formalized as lem_mod_of_prod2.

Sources

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

Leanlem_mod_of_prod2

Used by 1

Used byB modulus

LemmaB modulus#

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

Lean

Formalized as lem_mod_Bf_is_prod_mod.

Sources

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

Leanlem_mod_Bf_is_prod_mod

Uses 2 · Used by 2

Proof usesB off K · Mod product

Used byB at zero · B modulus

LemmaAbs power#

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

Lean

Formalized as lem_abs_pow.

Sources

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

Leanlem_abs_pow

Used by 1

Used byPower mod

LemmaPower mod#

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

Lean

Formalized as lem_Bmod_pow.

Sources

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

Leanlem_Bmod_pow

Uses 1 · Used by 1

Proof usesAbs power

Used byB modulus

LemmaB modulus#

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

Lean

Formalized as lem_mod_Bf_prod_mod.

Sources

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

Leanlem_mod_Bf_prod_mod

Uses 2

Proof usesB modulus · Power mod

LemmaB at zero#

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

Lean

Formalized as lem_mod_Bf_at_0.

Sources

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

Leanlem_mod_Bf_at_0

Uses 1 · Used by 1

Proof usesB modulus

Used byB zero form

LemmaAbs division#

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

Lean

Formalized as lem_mod_div_.

Sources

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

Leanlem_mod_div_

Used by 1

Used byAbs ratio

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.