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(measure_theory/function/l1_space): generalize multiplicative results to is_unit #19073

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - feat(measure_theory/function/l1_space): generalize multiplicative results to is_unit #19073

wants to merge 17 commits into from

Commits on May 23, 2023

  1. chore(measure_theory/function/l1_space): golf downstream results

    @eric-wieser
    eric-wieser committed May 23, 2023
    Configuration menu
    Copy the full SHA
    04d7099 View commit details
    Browse the repository at this point in the history

  2. more

    @eric-wieser
    eric-wieser committed May 23, 2023
    Configuration menu
    Copy the full SHA
    8b3dab3 View commit details
    Browse the repository at this point in the history

  3. missing root

    @eric-wieser
    eric-wieser committed May 23, 2023
    Configuration menu
    Copy the full SHA
    15fa6ba View commit details
    Browse the repository at this point in the history

  4. golf

    @eric-wieser
    eric-wieser committed May 23, 2023
    Configuration menu
    Copy the full SHA
    2626683 View commit details
    Browse the repository at this point in the history

  5. one more foundational lemma

    @eric-wieser
    eric-wieser committed May 23, 2023
    Configuration menu
    Copy the full SHA
    22d446a View commit details
    Browse the repository at this point in the history

  6. tweak style

    @eric-wieser
    eric-wieser committed May 23, 2023
    Configuration menu
    Copy the full SHA
    3589404 View commit details
    Browse the repository at this point in the history

Commits on May 24, 2023

  1. Update src/algebra/group/opposite.lean

    @eric-wieser
    eric-wieser committed May 24, 2023
    Configuration menu
    Copy the full SHA
    e3902e9 View commit details
    Browse the repository at this point in the history

  2. more generalizations

    @eric-wieser
    eric-wieser committed May 24, 2023
    Configuration menu
    Copy the full SHA
    3137c7a View commit details
    Browse the repository at this point in the history

  3. one more

    @eric-wieser
    eric-wieser committed May 24, 2023
    Configuration menu
    Copy the full SHA
    688c8a6 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into eric-wieser/bounded… 

    …-smul-cleanup
    @eric-wieser
    eric-wieser committed May 24, 2023
    Configuration menu
    Copy the full SHA
    5a189f9 View commit details
    Browse the repository at this point in the history

  5. Merge remote-tracking branch 'origin/master' into eric-wieser/bounded… 

    …-smul-cleanup
    @eric-wieser
    eric-wieser committed May 24, 2023
    Configuration menu
    Copy the full SHA
    46f9f8d View commit details
    Browse the repository at this point in the history

  6. small generalization

    @eric-wieser
    eric-wieser committed May 24, 2023
    Configuration menu
    Copy the full SHA
    3e5763e View commit details
    Browse the repository at this point in the history

Commits on May 26, 2023

  1. Merge remote-tracking branch 'origin/staging' into eric-wieser/bounde… 

    …d-smul-cleanup
    @eric-wieser
    eric-wieser committed May 26, 2023
    Configuration menu
    Copy the full SHA
    dfd463d View commit details
    Browse the repository at this point in the history

  2. generalize the rest

    @eric-wieser
    eric-wieser committed May 26, 2023
    Configuration menu
    Copy the full SHA
    a3cee72 View commit details
    Browse the repository at this point in the history

  3. Generalize a bunch of downstream file too

    @eric-wieser
    eric-wieser committed May 26, 2023
    Configuration menu
    Copy the full SHA
    a961813 View commit details
    Browse the repository at this point in the history

Commits on May 27, 2023

  1. revert less-motivated changes

    @eric-wieser
    eric-wieser committed May 27, 2023
    Configuration menu
    Copy the full SHA
    9c660aa View commit details
    Browse the repository at this point in the history

  2. fix

    @eric-wieser
    eric-wieser committed May 27, 2023
    Configuration menu
    Copy the full SHA
    747be94 View commit details
    Browse the repository at this point in the history