1 search result for "tag:"logpath:pi_leibniz""

Showing 1 - 1
  1. 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