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: compute Monoid.exponent as the lcm over pi types and Prod #8066

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat: compute Monoid.exponent as the lcm over pi types and Prod #8066

wants to merge 5 commits into from

Commits on Oct 31, 2023

  1. feat: compute Monoid.exponent as the lcm over pi types and Prod

    @j-loreaux
    j-loreaux committed Oct 31, 2023
    Configuration menu
    Copy the full SHA
    2496a29 View commit details
    Browse the repository at this point in the history

  2. remove unnecessary lemma

    @j-loreaux
    j-loreaux committed Oct 31, 2023
    Configuration menu
    Copy the full SHA
    ec2686c View commit details
    Browse the repository at this point in the history

Commits on Nov 1, 2023

  1. switch from Nat.lcm to lcm

    @j-loreaux
    j-loreaux committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    fec5d7b View commit details
    Browse the repository at this point in the history

  2. add docstrings and module doc

    @j-loreaux
    j-loreaux committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    875176e View commit details
    Browse the repository at this point in the history

  3. code review 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @j-loreaux @eric-wieser
    j-loreaux and eric-wieser committed Nov 1, 2023
    Configuration menu
    Copy the full SHA
    403589d View commit details
    Browse the repository at this point in the history