audit-session028-axioms.txt
22 declarations audited · 3 standard axioms only · updated 08-23-2026
Raw #print axioms transcript
'NguyenRH1.seriesTerm' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesFun' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.one_add_normSq_gammaOf_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.one_div_sub_add_one_div' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesTerm_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.finite_subtype_norm_lt' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesTerm_summable_majorant' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesSummable' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.exists_ball_avoid_nontrivialZeros' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesFun_analyticAt' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesFun_analyticOnNhd' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.nontrivialZero_isolated' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesTermSub' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesFunSub' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesTermSub_norm_le' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesTermSub_summable' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.single_summable' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesFun_eq_sub_add' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesFun_sub_term' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesFunSub_analyticAt' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesFun_sub_self_term_analyticAt' depends on axioms: [propext, Classical.choice, Quot.sound] 'NguyenRH1.seriesFun_sub_polar_analyticAt' depends on axioms: [propext, Classical.choice, Quot.sound]