Repository navigation
Companion note, version 1.8
Adds Appendix A rows for two statements the note already made, now machine-checked: Diaz 1997, Proposition 1 (DiazModulus.log_pair_algebraicIndependent_of_mul_eq_rat_pi_sq), and Waldschmidt's Consequence 1.6 under the strong four exponentials conjecture (DiazModulus.div_not_mem_logAlgTilde_of_sfe, which proves Consequence 1.7). The mirrored library holds 229 results.