Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: super factorial #6768

Closed
wants to merge 13 commits into from
Closed

[Merged by Bors] - feat: super factorial #6768

wants to merge 13 commits into from

Commits on Aug 24, 2023

  1. feat: super factorial

    @mo271
    mo271 committed Aug 24, 2023
    Configuration menu
    Copy the full SHA
    cf34ebf View commit details
    Browse the repository at this point in the history

  2. minimize imports

    @mo271
    mo271 committed Aug 24, 2023
    Configuration menu
    Copy the full SHA
    ecd856e View commit details
    Browse the repository at this point in the history

  3. mv file

    @mo271
    mo271 committed Aug 24, 2023
    Configuration menu
    Copy the full SHA
    48de13f View commit details
    Browse the repository at this point in the history

  4. doc

    @mo271
    mo271 committed Aug 24, 2023
    Configuration menu
    Copy the full SHA
    567a39b View commit details
    Browse the repository at this point in the history

Commits on Aug 26, 2023

  1. Update Mathlib/Data/Nat/Factorial/SuperFactorial.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @mo271 @eric-wieser
    mo271 and eric-wieser committed Aug 26, 2023
    Configuration menu
    Copy the full SHA
    c9bf4cc View commit details
    Browse the repository at this point in the history

  2. super_factorial -> superFactorial

    @mo271
    mo271 committed Aug 26, 2023
    Configuration menu
    Copy the full SHA
    96652ff View commit details
    Browse the repository at this point in the history

Commits on Aug 30, 2023

  1. Update Mathlib/Data/Nat/Factorial/SuperFactorial.lean

    @mo271
    mo271 committed Aug 30, 2023
    Configuration menu
    Copy the full SHA
    b8e3c50 View commit details
    Browse the repository at this point in the history

  2. Apply suggestions from code review

    @mo271
    mo271 committed Aug 30, 2023
    Configuration menu
    Copy the full SHA
    51ece51 View commit details
    Browse the repository at this point in the history

  3. add precedence

    @mo271
    mo271 committed Aug 30, 2023
    Configuration menu
    Copy the full SHA
    420e696 View commit details
    Browse the repository at this point in the history

  4. link to wikipedia and different spelling

    @mo271
    mo271 committed Aug 30, 2023
    Configuration menu
    Copy the full SHA
    475b54c View commit details
    Browse the repository at this point in the history

  5. fix precedence

    @mo271
    mo271 committed Aug 30, 2023
    Configuration menu
    Copy the full SHA
    5459d4a View commit details
    Browse the repository at this point in the history

  6. remove simp

    @mo271
    mo271 committed Aug 30, 2023
    Configuration menu
    Copy the full SHA
    1494a4a View commit details
    Browse the repository at this point in the history

  7. mention sf notation

    @mo271
    mo271 committed Aug 30, 2023
    Configuration menu
    Copy the full SHA
    3c64e8e View commit details
    Browse the repository at this point in the history