Skip to content

History

Revisions

  • Simplify the instructions for lakefile edits

    @eric-wieser eric-wieser committed May 7, 2026
    829628a

  • `Π x : A, P x` is available now

    @Komyyy Komyyy committed May 1, 2026
    414be2d

  • Updated Globally shared mathlib installation (markdown)

    @joneugster joneugster committed Feb 3, 2026
    aa84a8f

  • Updated Project setup following stable releases (markdown)

    @joneugster joneugster committed Feb 3, 2026
    5fec89c

  • Created Project setup: using local development version of a dependency (markdown)

    @joneugster joneugster committed Feb 3, 2026
    30eda8d

  • Created Project setup following stable releases (markdown)

    @joneugster joneugster committed Feb 3, 2026
    1f0bb0f

  • Created Globally shared mathlib installation (markdown)

    @joneugster joneugster committed Feb 3, 2026
    61397ed

  • Fix a typo

    @grunweg grunweg committed Dec 7, 2025
    4c43f26

  • mention syntax refs

    @kmill kmill committed Aug 28, 2025
    38ec376

  • Tutorial on lint and test drivers in the Lakefile.

    @Vierkantor Vierkantor committed Jun 26, 2025
    0f6884f

  • Created Migration to PRs from forks (markdown)

    @jcommelin jcommelin committed Jun 18, 2025
    f725164

  • add a link to a Zulip discussion

    @alreadydone alreadydone committed Jun 3, 2025
    05ba40e

  • Updated Computation models for polynomials and finitely supported functions (markdown)

    @eric-wieser eric-wieser committed May 27, 2025
    5411611

  • Updated Computation models for polynomials and finitely supported functions (markdown)

    @eric-wieser eric-wieser committed May 27, 2025
    ae7be21

  • Updated Using mathlib4 as a dependency (markdown)

    @ldct ldct committed May 17, 2025
    f007f42

  • Updated RFC: drop `Nat.AtLeastTwo` (markdown)

    @kim-em kim-em committed Apr 10, 2025
    33a5f00

  • Updated RFC: drop `Nat.AtLeastTwo` (markdown)

    @urkud urkud committed Apr 10, 2025
    2e7ee21

  • Updated RFC: drop `Nat.AtLeastTwo` (markdown)

    @urkud urkud committed Apr 10, 2025
    b250392

  • Updated RFC: drop `Nat.AtLeastTwo` (markdown)

    @eric-wieser eric-wieser committed Apr 9, 2025
    058e99b

  • Created RFC: drop `Nat.AtLeastTwo` (markdown)

    @urkud urkud committed Apr 9, 2025
    0630d5c

  • 1. Fix the direction of EIO & IO arrow 2. Clarify the direction of arrows in the text 3. Make solid arrows bold

    @lakesare lakesare committed Apr 9, 2025
    8aacfbf

  • Link the tracking issue.

    @eric-wieser eric-wieser committed Apr 7, 2025
    6601ab9

  • add comments about minimizing imports

    @j-loreaux j-loreaux committed Apr 7, 2025
    e20a509

  • Created RFC/Exp function (markdown)

    @urkud urkud committed Apr 7, 2025
    4f30c9b

  • Fix typo Commmand -> Command

    @b-mehta b-mehta committed Mar 29, 2025
    699cd6b

  • Updated Metaprogramming gotchas (markdown)

    @kmill kmill committed Mar 4, 2025
    4279505

  • Updated Metaprogramming gotchas (markdown)

    @kmill kmill committed Mar 4, 2025
    3ae71d0

  • Updated Metaprogramming gotchas (markdown)

    @kmill kmill committed Mar 4, 2025
    a16cd97

  • Updated Metaprogramming gotchas (markdown)

    @kmill kmill committed Jan 14, 2025
    2882c09

  • Updated Using mathlib4 as a dependency (markdown)

    @kim-em kim-em committed Dec 3, 2024
    90d792e