Skip to content

History

Revisions

  • 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

  • Write Tradeoffs of concrete types defined as subobjects

    @YaelDillies YaelDillies committed Jul 25, 2024
    6e895c4

  • Destroyed port comments (markdown)

    @jcommelin jcommelin committed Jul 18, 2024
    aaed9b5

  • Updated Working with dependent PRs (markdown)

    @eric-wieser eric-wieser committed Jul 2, 2024
    014de59

  • Updated Working with dependent PRs (markdown)

    @eric-wieser eric-wieser committed Jul 2, 2024
    d77de61

  • Updated Working with dependent PRs (markdown)

    @eric-wieser eric-wieser committed Jul 2, 2024
    cd791db

  • Updated Working with dependent PRs (markdown)

    @eric-wieser eric-wieser committed Jul 2, 2024
    5ad3aaf