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

feat(Analysis/InnerProductSpace/Dual, Mathlib/Analysis/Normed/Group/SeparationQuotient): add null submodule and various lifts #16707

Open
wants to merge 58 commits into
base: master
Choose a base branch
from
Open

feat(Analysis/InnerProductSpace/Dual, Mathlib/Analysis/Normed/Group/SeparationQuotient): add null submodule and various lifts #16707

wants to merge 58 commits into from
+318 −5

Commits on Sep 6, 2024

  1. put Semi

    @yoh-tanimoto
    yoh-tanimoto authored Sep 6, 2024
    Configuration menu
    Copy the full SHA
    58dbb79 View commit details
    Browse the repository at this point in the history

  2. put Semi

    @yoh-tanimoto
    yoh-tanimoto authored Sep 6, 2024
    Configuration menu
    Copy the full SHA
    cbe33c3 View commit details
    Browse the repository at this point in the history

Commits on Sep 8, 2024

  1. Create Quotient.lean

    @yoh-tanimoto
    yoh-tanimoto authored Sep 8, 2024
    Configuration menu
    Copy the full SHA
    e973783 View commit details
    Browse the repository at this point in the history

Commits on Sep 10, 2024

  1. Update Quotient.lean

    @yoh-tanimoto
    yoh-tanimoto authored Sep 10, 2024
    Configuration menu
    Copy the full SHA
    01c83b1 View commit details
    Browse the repository at this point in the history

  2. Update Quotient.lean

    @yoh-tanimoto
    yoh-tanimoto authored Sep 10, 2024
    Configuration menu
    Copy the full SHA
    ef8ba7c View commit details
    Browse the repository at this point in the history

  3. add line to Mathlib.lean

    @yoh-tanimoto
    yoh-tanimoto authored Sep 10, 2024
    Configuration menu
    Copy the full SHA
    57289ae View commit details
    Browse the repository at this point in the history

  4. add docstring

    @yoh-tanimoto
    yoh-tanimoto authored Sep 10, 2024
    Configuration menu
    Copy the full SHA
    795b1a3 View commit details
    Browse the repository at this point in the history

Commits on Sep 12, 2024

  1. Update Mathlib/Analysis/InnerProductSpace/Quotient.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @yoh-tanimoto @eric-wieser
    yoh-tanimoto and eric-wieser authored Sep 12, 2024
    Configuration menu
    Copy the full SHA
    b3d12f0 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Analysis/InnerProductSpace/Quotient.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @yoh-tanimoto @eric-wieser
    yoh-tanimoto and eric-wieser authored Sep 12, 2024
    Configuration menu
    Copy the full SHA
    5432128 View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/Analysis/InnerProductSpace/Quotient.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @yoh-tanimoto @eric-wieser
    yoh-tanimoto and eric-wieser authored Sep 12, 2024
    Configuration menu
    Copy the full SHA
    77411bd View commit details
    Browse the repository at this point in the history

  4. Update Mathlib/Analysis/InnerProductSpace/Quotient.lean 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @yoh-tanimoto @eric-wieser
    yoh-tanimoto and eric-wieser authored Sep 12, 2024
    Configuration menu
    Copy the full SHA
    e9ded34 View commit details
    Browse the repository at this point in the history

  5. Update Quotient.lean

    @yoh-tanimoto
    yoh-tanimoto authored Sep 12, 2024
    Configuration menu
    Copy the full SHA
    130243e View commit details
    Browse the repository at this point in the history

Commits on Sep 25, 2024

  1. Merge remote-tracking branch 'origin/master' into yoh-tanimoto-innerp… 

    …roductspace-quotient
    @eric-wieser
    eric-wieser committed Sep 25, 2024
    Configuration menu
    Copy the full SHA
    72dd13e View commit details
    Browse the repository at this point in the history

Commits on Sep 26, 2024

  1. Merge pull request #17157 from leanprover-community/master 

    sync to master
    @yoh-tanimoto
    yoh-tanimoto authored Sep 26, 2024
    Configuration menu
    Copy the full SHA
    a1a093f View commit details
    Browse the repository at this point in the history

  2. Update Quotient.lean

    @yoh-tanimoto
    yoh-tanimoto authored Sep 26, 2024
    Configuration menu
    Copy the full SHA
    1d99e4b View commit details
    Browse the repository at this point in the history

Commits on Sep 30, 2024

  1. Merge remote-tracking branch 'origin/master' into yoh-tanimoto-innerp… 

    …roductspace-quotient
    @yoh-tanimoto
    yoh-tanimoto committed Sep 30, 2024
    Configuration menu
    Copy the full SHA
    9e29b5d View commit details
    Browse the repository at this point in the history

Commits on Oct 2, 2024

  1. Create SeparationQuotient.lean 

    unfinished
    @yoh-tanimoto
    yoh-tanimoto authored Oct 2, 2024
    Configuration menu
    Copy the full SHA
    1afcd2b View commit details
    Browse the repository at this point in the history

  2. Update SeparationQuotient.lean

    @yoh-tanimoto
    yoh-tanimoto authored Oct 2, 2024
    Configuration menu
    Copy the full SHA
    3badb3f View commit details
    Browse the repository at this point in the history

  3. Update Mathlib.lean

    @yoh-tanimoto
    yoh-tanimoto authored Oct 2, 2024
    Configuration menu
    Copy the full SHA
    f39b370 View commit details
    Browse the repository at this point in the history

  4. rename

    @yoh-tanimoto
    yoh-tanimoto authored Oct 2, 2024
    Configuration menu
    Copy the full SHA
    89b7fd6 View commit details
    Browse the repository at this point in the history

  5. replace namespace

    @yoh-tanimoto
    yoh-tanimoto authored Oct 2, 2024
    Configuration menu
    Copy the full SHA
    115541f View commit details
    Browse the repository at this point in the history

  6. add namespace

    @yoh-tanimoto
    yoh-tanimoto authored Oct 2, 2024
    Configuration menu
    Copy the full SHA
    5186e8a View commit details
    Browse the repository at this point in the history

Commits on Oct 3, 2024

  1. Update Mathlib/Analysis/Normed/Group/SeparationQuotient.lean 

    Co-authored-by: Eric Wieser <efw@google.com>
    @yoh-tanimoto @eric-wieser
    yoh-tanimoto and eric-wieser authored Oct 3, 2024
    Configuration menu
    Copy the full SHA
    358d5c8 View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/Analysis/Normed/Group/SeparationQuotient.lean 

    Co-authored-by: Eric Wieser <efw@google.com>
    @yoh-tanimoto @eric-wieser
    yoh-tanimoto and eric-wieser authored Oct 3, 2024
    Configuration menu
    Copy the full SHA
    6233160 View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/Analysis/Normed/Group/SeparationQuotient.lean 

    Co-authored-by: Eric Wieser <efw@google.com>
    @yoh-tanimoto @eric-wieser
    yoh-tanimoto and eric-wieser authored Oct 3, 2024
    Configuration menu
    Copy the full SHA
    b9e8354 View commit details
    Browse the repository at this point in the history

  4. Update SeparationQuotient.lean

    @yoh-tanimoto
    yoh-tanimoto authored Oct 3, 2024
    Configuration menu
    Copy the full SHA
    dceb20e View commit details
    Browse the repository at this point in the history

  5. use SetLike.mem_coe

    @yoh-tanimoto
    yoh-tanimoto authored Oct 3, 2024
    Configuration menu
    Copy the full SHA
    a5f395a View commit details
    Browse the repository at this point in the history

  6. Update Mathlib/Topology/Algebra/SeparationQuotient.lean 

    Co-authored-by: Eric Wieser <efw@google.com>
    @yoh-tanimoto @eric-wieser
    yoh-tanimoto and eric-wieser authored Oct 3, 2024
    Configuration menu
    Copy the full SHA
    18b3510 View commit details
    Browse the repository at this point in the history

  7. Update Mathlib/Topology/Algebra/SeparationQuotient.lean 

    Co-authored-by: Eric Wieser <efw@google.com>
    @yoh-tanimoto @eric-wieser
    yoh-tanimoto and eric-wieser authored Oct 3, 2024
    Configuration menu
    Copy the full SHA
    a2dc60e View commit details
    Browse the repository at this point in the history

  8. Update Mathlib/Topology/Algebra/SeparationQuotient.lean 

    Co-authored-by: Eric Wieser <efw@google.com>
    @yoh-tanimoto @eric-wieser
    yoh-tanimoto and eric-wieser authored Oct 3, 2024
    Configuration menu
    Copy the full SHA
    a80e621 View commit details
    Browse the repository at this point in the history

  9. Revert "Update Mathlib/Topology/Algebra/SeparationQuotient.lean" 

    This reverts commit a80e621.
    @yoh-tanimoto
    yoh-tanimoto committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    cd58b59 View commit details
    Browse the repository at this point in the history

  10. change names

    @yoh-tanimoto
    yoh-tanimoto committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    bfb096c View commit details
    Browse the repository at this point in the history

  11. add liftCLM and others

    @yoh-tanimoto
    yoh-tanimoto committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    ce9ce50 View commit details
    Browse the repository at this point in the history

  12. Update Mathlib.lean

    @yoh-tanimoto
    yoh-tanimoto committed Oct 3, 2024
    Configuration menu
    Copy the full SHA
    cde0e53 View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2024

  1. add liftCLM

    @yoh-tanimoto
    yoh-tanimoto committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    006c9f8 View commit details
    Browse the repository at this point in the history

  2. done InnerProductSpace

    @yoh-tanimoto
    yoh-tanimoto committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    b2a3322 View commit details
    Browse the repository at this point in the history

Commits on Oct 5, 2024

  1. Merge branch 'master' into yoh-tanimoto-innerproductspace-quotient

    @yoh-tanimoto
    yoh-tanimoto authored Oct 5, 2024
    Configuration menu
    Copy the full SHA
    f06620b View commit details
    Browse the repository at this point in the history

  2. modify namespaces, docstring

    @yoh-tanimoto
    yoh-tanimoto committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    a51f01b View commit details
    Browse the repository at this point in the history

  3. remove unnecessary variables, add docstring

    @yoh-tanimoto
    yoh-tanimoto committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    467554a View commit details
    Browse the repository at this point in the history

  4. Update SeparationQuotient.lean

    @yoh-tanimoto
    yoh-tanimoto committed Oct 5, 2024
    Configuration menu
    Copy the full SHA
    6b2e073 View commit details
    Browse the repository at this point in the history

Commits on Oct 9, 2024

  1. Merge remote-tracking branch 'origin/master' into yoh-tanimoto-innerp… 

    …roductspace-quotient
    @yoh-tanimoto
    yoh-tanimoto committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    1ad7a36 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into yoh-tanimoto-innerp… 

    …roductspace-quotient
    @yoh-tanimoto
    yoh-tanimoto committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    e85a785 View commit details
    Browse the repository at this point in the history

  3. clean up contents after #17452 and #17576

    @yoh-tanimoto
    yoh-tanimoto committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    a684b79 View commit details
    Browse the repository at this point in the history

  4. min_imports

    @yoh-tanimoto
    yoh-tanimoto committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    efa6dbf View commit details
    Browse the repository at this point in the history

Commits on Oct 13, 2024

  1. clean up

    @yoh-tanimoto
    yoh-tanimoto committed Oct 13, 2024
    Configuration menu
    Copy the full SHA
    1be4b62 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into yoh-tanimoto-innerproductspace-quotient

    @yoh-tanimoto
    yoh-tanimoto committed Oct 13, 2024
    Configuration menu
    Copy the full SHA
    4c9fda2 View commit details
    Browse the repository at this point in the history

  3. Update Mathlib.lean 

    Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
    @yoh-tanimoto @github-actions
    yoh-tanimoto and github-actions[bot] authored Oct 13, 2024
    Configuration menu
    Copy the full SHA
    cd0a7c7 View commit details
    Browse the repository at this point in the history

  4. clean up

    @yoh-tanimoto
    yoh-tanimoto committed Oct 13, 2024
    Configuration menu
    Copy the full SHA
    fcee1dd View commit details
    Browse the repository at this point in the history

  5. #min_imports

    @yoh-tanimoto
    yoh-tanimoto committed Oct 13, 2024
    Configuration menu
    Copy the full SHA
    b684eda View commit details
    Browse the repository at this point in the history

  6. Update SeparationQuotient.lean

    @yoh-tanimoto
    yoh-tanimoto committed Oct 13, 2024
    Configuration menu
    Copy the full SHA
    b148d6d View commit details
    Browse the repository at this point in the history

Commits on Oct 20, 2024

  1. Merge branch 'master' into yoh-tanimoto-innerproductspace-quotient

    @yoh-tanimoto
    yoh-tanimoto authored Oct 20, 2024
    Configuration menu
    Copy the full SHA
    748c4c8 View commit details
    Browse the repository at this point in the history

  2. golf

    @eric-wieser
    eric-wieser committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    ee93929 View commit details
    Browse the repository at this point in the history

  3. golf again

    @eric-wieser
    eric-wieser committed Oct 20, 2024
    Configuration menu
    Copy the full SHA
    e0292b6 View commit details
    Browse the repository at this point in the history

Commits on Oct 22, 2024

  1. Update Mathlib/Analysis/InnerProductSpace/Dual.lean 

    Co-authored-by: Eric Wieser <efw@google.com>
    @yoh-tanimoto @eric-wieser
    yoh-tanimoto and eric-wieser authored Oct 22, 2024
    Configuration menu
    Copy the full SHA
    7245c69 View commit details
    Browse the repository at this point in the history

  2. various

    @yoh-tanimoto
    yoh-tanimoto committed Oct 22, 2024
    Configuration menu
    Copy the full SHA
    1329bfe View commit details
    Browse the repository at this point in the history

  3. Update SeparationQuotient.lean

    @yoh-tanimoto
    yoh-tanimoto committed Oct 22, 2024
    Configuration menu
    Copy the full SHA
    3ea9891 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into yoh-tanimoto-innerproductspace-quotient

    @yoh-tanimoto
    yoh-tanimoto committed Oct 22, 2024
    Configuration menu
    Copy the full SHA
    ceee774 View commit details
    Browse the repository at this point in the history

  5. #min_imports

    @yoh-tanimoto
    yoh-tanimoto committed Oct 22, 2024
    Configuration menu
    Copy the full SHA
    6b20162 View commit details
    Browse the repository at this point in the history