2 search results for "tag:"keyword:irrationality""

Showing 1 - 2
  1. coq-mathcomp-apery

    No documentation

    A formally verified proof in Coq, by computer algebra, that ζ(3) is irrational
    category:Mathematics/Arithmetic and Number Theory/Number theory keyword:apery recurrence keyword:irrationality keyword:creative telescoping logpath:mathcomp.apery date:2022-05-05
    Frédéric Chyzak Assia Mahboubi Thomas Sibut-Pinote
    1.0.2
    CECILL-C
    Used by 0 other packages
    05 May 2022
  2. rocq-pi-leibniz

    No documentation

    Constructive pi for the Rocq constructive Cauchy reals with premise-free rational separation
    keyword:pi keyword:constructive reals keyword:irrationality date:2026-10-15 logpath:pi_leibniz
    Wang Baojun <168888@live.cn> Zhou Zhinong <zrm2000@126.com> Zeng Baiyuan <3052633793@qq.com>
    1.0.0
    LGPL-2.1
    Used by 0 other packages
    20 Oct 2026