audit-session027b-axioms.txt
11 declarations audited · 3 standard axioms only · updated 08-23-2026
Raw #print axioms transcript
'NguyenRH1.sum_range_one_div_sub' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.hasSum_one_div_sub_telescope' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.tsum_one_div_sub_telescope' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.digamma_natCast_eq' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.summable_digamma_majorant' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_digamma_term_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.sum_one_div_le_one_add_log' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.norm_digamma_le_of_two_le_re' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.recip_norm_le_right' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.recip_norm_le_left' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.digamma_recip_sum_le' depends on axioms: [propext, Classical.choice, Quot.sound]