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(analysis/matrix): define the frobenius norm on matrices #13497

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - feat(analysis/matrix): define the frobenius norm on matrices #13497

wants to merge 17 commits into from

Commits on Apr 17, 2022

  1. chore(analysis/normed_space/finite_dimension): golf a proof 

    These `letI`s just made this proof convoluted, the instances were not needed.
Similarly, the `classical` was the cause of the need for the `congr`.
    @eric-wieser
    eric-wieser committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    f12e181 View commit details
    Browse the repository at this point in the history

Commits on Apr 18, 2022

  1. chore(analysis): lemmas about nnorm

    @eric-wieser
    eric-wieser committed Apr 18, 2022
    Configuration menu
    Copy the full SHA
    321d06d View commit details
    Browse the repository at this point in the history

  2. wip

    @eric-wieser
    eric-wieser committed Apr 18, 2022
    Configuration menu
    Copy the full SHA
    d9530b6 View commit details
    Browse the repository at this point in the history

  3. wip

    @eric-wieser
    eric-wieser committed Apr 18, 2022
    Configuration menu
    Copy the full SHA
    403f25b View commit details
    Browse the repository at this point in the history

  4. fix

    @eric-wieser
    eric-wieser committed Apr 18, 2022
    Configuration menu
    Copy the full SHA
    0fa629b View commit details
    Browse the repository at this point in the history

  5. helper lemma

    @eric-wieser
    eric-wieser committed Apr 18, 2022
    Configuration menu
    Copy the full SHA
    49c7a71 View commit details
    Browse the repository at this point in the history

Commits on Apr 19, 2022

  1. Merge branch 'master' into eric-wieser/matrix-frobenius

    @eric-wieser
    eric-wieser committed Apr 19, 2022
    Configuration menu
    Copy the full SHA
    b692fe2 View commit details
    Browse the repository at this point in the history

  2. Update basic.lean

    @eric-wieser
    eric-wieser committed Apr 19, 2022
    Configuration menu
    Copy the full SHA
    0ad8a3e View commit details
    Browse the repository at this point in the history

Commits on Apr 20, 2022

  1. fix lemma names

    @eric-wieser
    eric-wieser committed Apr 20, 2022
    Configuration menu
    Copy the full SHA
    bdf7e7d View commit details
    Browse the repository at this point in the history

Commits on Apr 21, 2022

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/matrix-… 

    …frobenius
    @eric-wieser
    eric-wieser committed Apr 21, 2022
    Configuration menu
    Copy the full SHA
    1b4588e View commit details
    Browse the repository at this point in the history

  2. wip

    @eric-wieser
    eric-wieser committed Apr 21, 2022
    Configuration menu
    Copy the full SHA
    3af3114 View commit details
    Browse the repository at this point in the history

  3. feat(analysis/normed_space/pi_Lp): add lemmas about pi_Lp.equiv 

    Most of these are trivial dsimp lemmas, but they also let us talk about the norm of constant vectors.
    @eric-wieser
    eric-wieser committed Apr 21, 2022
    Configuration menu
    Copy the full SHA
    8487e2b View commit details
    Browse the repository at this point in the history

Commits on Apr 22, 2022

  1. Merge remote-tracking branch 'origin/master' into eric-wieser/matrix-… 

    …frobenius
    @eric-wieser
    eric-wieser committed Apr 22, 2022
    Configuration menu
    Copy the full SHA
    449e650 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/eric-wieser/pi_Lp-lemmas' into e… 

    …ric-wieser/matrix-frobenius
    @eric-wieser
    eric-wieser committed Apr 22, 2022
    Configuration menu
    Copy the full SHA
    e72114e View commit details
    Browse the repository at this point in the history

Commits on Apr 29, 2022

  1. Merge branch 'master' into eric-wieser/matrix-frobenius

    @eric-wieser
    eric-wieser committed Apr 29, 2022
    Configuration menu
    Copy the full SHA
    6b8d1ec View commit details
    Browse the repository at this point in the history

  2. Fix lemma name

    @eric-wieser
    eric-wieser committed Apr 29, 2022
    Configuration menu
    Copy the full SHA
    02cac1d View commit details
    Browse the repository at this point in the history

  3. fix

    @eric-wieser
    eric-wieser committed Apr 29, 2022
    Configuration menu
    Copy the full SHA
    8075b03 View commit details
    Browse the repository at this point in the history