Skip to content

History

Revisions

  • 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

  • Switch to a horizontal layout for clearer labels.

    @eric-wieser eric-wieser committed Oct 22, 2024
    45dc74c

  • Fix typo

    @eric-wieser eric-wieser committed Oct 22, 2024
    5ea6d77

  • Add liftCommandElabM

    @eric-wieser eric-wieser committed Oct 22, 2024
    9b8aa96

  • We've got way more than 2k files in Mathlib nowadays.

    @vihdzp vihdzp committed Sep 8, 2024
    49d8a50

  • Corrected spelling of practice

    @faenuccio faenuccio committed Aug 26, 2024
    ac78126

  • Improved syntax.

    @faenuccio faenuccio committed Aug 26, 2024
    ff1bf55

  • Changed return to pure in the second line.

    @faenuccio faenuccio committed Aug 26, 2024
    dd914cf

  • Updated Using mathlib4 as a dependency (markdown)

    @Ruben-VandeVelde Ruben-VandeVelde committed Aug 21, 2024
    17cc8bd