Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

feat(measure_theory/measure/haar_lebesgue): the volume measures on euclidean_space ℝ ι and ι → ℝ agree #19013

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

feat(measure_theory/measure/haar_lebesgue): the volume measures on euclidean_space ℝ ι and ι → ℝ agree #19013

wants to merge 21 commits into from

Commits on Apr 26, 2023

  1. feat(measure_theory/measure/haar_of_basis): put the canonical measure… 

    … on euclidean space
    @eric-wieser
    eric-wieser committed Apr 26, 2023
    Configuration menu
    Copy the full SHA
    b9e8712 View commit details
    Browse the repository at this point in the history

  2. add lemma

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

  3. wip

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

  4. wip

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

  5. feat(topology/sets/compacts): add positive_compacts.map 

    Also adds some missing functorial lemmas about `map`
    @eric-wieser
    eric-wieser committed Apr 26, 2023
    Configuration menu
    Copy the full SHA
    358d353 View commit details
    Browse the repository at this point in the history

  6. chore(measure_theory/measure/haar_of_basis): lemmas about `basis.para… 

    …llelepiped`

These are bundled versions of the lemmas about `parallelepiped`.
    @eric-wieser
    eric-wieser committed Apr 26, 2023
    Configuration menu
    Copy the full SHA
    6ed508e View commit details
    Browse the repository at this point in the history

Commits on May 12, 2023

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

    …-basis.parallelepiped-lemmas
    @eric-wieser
    eric-wieser committed May 12, 2023
    Configuration menu
    Copy the full SHA
    f8ab07b View commit details
    Browse the repository at this point in the history

Commits on May 14, 2023

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

    …an-measurable-2
    @eric-wieser
    eric-wieser committed May 14, 2023
    Configuration menu
    Copy the full SHA
    f5bb3b5 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/eric-wieser/trivial-basis.parall… 

    …elepiped-lemmas' into eric-wieser/euclidean-measurable-2
    @eric-wieser
    eric-wieser committed May 14, 2023
    Configuration menu
    Copy the full SHA
    0680ec1 View commit details
    Browse the repository at this point in the history

  3. fix bad merge

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

Commits on May 15, 2023

  1. wip

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

  2. Merge remote-tracking branch 'origin/master' into eric-wieser/euclide… 

    …an-measurable-2
    @eric-wieser
    eric-wieser committed May 15, 2023
    Configuration menu
    Copy the full SHA
    e47004c View commit details
    Browse the repository at this point in the history

  3. reduce diff

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

  4. wip

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

  5. whoops, sloppy types

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

  6. remove bad lemma

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

  7. wip

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

  8. revert unrelated tweaks

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

Commits on May 22, 2023

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

    …an-measurable-2
    @eric-wieser
    eric-wieser committed May 22, 2023
    Configuration menu
    Copy the full SHA
    2d45663 View commit details
    Browse the repository at this point in the history

  2. wip

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

Commits on Jul 15, 2023

  1. new lemma

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