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

[Merged by Bors] - chore(measure_theory/measure/haar_of_basis): lemmas about basis.parallelepiped #18873

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - chore(measure_theory/measure/haar_of_basis): lemmas about basis.parallelepiped #18873

wants to merge 3 commits into from

Commits on Apr 26, 2023

  1. 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

  2. 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