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: remove the diamond for Complex.measureSpace #6832

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - feat: remove the diamond for Complex.measureSpace #6832

Changes from 3 commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
ed5dff2
1st commit
xroblot Aug 28, 2023
95b2f22
Merge remote-tracking branch 'origin' into xfr_complex_measure_ishaar
xroblot Sep 2, 2023
ff02d50
Review
xroblot Sep 2, 2023
b974b15
New version
xroblot Sep 5, 2023
fdec608
Fix imports
xroblot Sep 5, 2023
820f44a
Lint
xroblot Sep 5, 2023
2df6385
Add results from #19013
xroblot Sep 5, 2023
9139831
Clean up
xroblot Sep 5, 2023
2b24e48
clean up + docstring
xroblot Sep 5, 2023
eec4fcf
clean up
xroblot Sep 5, 2023
97fb274
adjust hypothesis
xroblot Sep 5, 2023
1766342
1st commit
xroblot Sep 8, 2023
01b073e
Clean up
xroblot Sep 8, 2023
f4fd951
Whitespace
xroblot Sep 8, 2023
4b1844e
Merge remote-tracking branch 'origin/xfr_haartools' into xfr_complex_…
xroblot Sep 8, 2023
a48fdff
Merge remote-tracking branch 'origin' into xfr_complex_measure_ishaar
xroblot Sep 12, 2023
0b537a1
Clean up after merge
xroblot Sep 12, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions Mathlib/MeasureTheory/Measure/Lebesgue/Complex.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,7 @@ Copyright (c) 2021 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
import Mathlib.MeasureTheory.Constructions.BorelSpace.Complex
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.MeasureTheory.Measure.Haar.OfBasis
import Mathlib.MeasureTheory.Measure.Haar.NormedSpace

#align_import measure_theory.measure.lebesgue.complex from "leanprover-community/mathlib"@"fd5edc43dc4f10b85abfe544b88f82cf13c5f844"

Expand Down Expand Up @@ -49,4 +47,6 @@ theorem volume_preserving_equiv_real_prod : MeasurePreserving measurableEquivRea
(volume_preserving_finTwoArrow ℝ).comp volume_preserving_equiv_pi
#align complex.volume_preserving_equiv_real_prod Complex.volume_preserving_equiv_real_prod

instance : Measure.IsAddHaarMeasure (@volume ℂ _) := Measure.MapLinearEquiv.isAddHaarMeasure _ _

end Complex
Loading