feat: port MeasureTheory.PiSystem (#2160)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Pol_tta <52843868+Komyyy@users.noreply.github.com>
leanprover-community · Feb 11, 2023 · 9a3cb30 · 9a3cb30
1 parent 4be13d0
commit 9a3cb30
Show file tree

Hide file tree

Showing 2 changed files with 766 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -790,6 +790,7 @@ import Mathlib.Mathport.Rename
 import Mathlib.Mathport.Syntax
 import Mathlib.MeasureTheory.MeasurableSpace
 import Mathlib.MeasureTheory.MeasurableSpaceDef
+import Mathlib.MeasureTheory.PiSystem
 import Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
 import Mathlib.NumberTheory.Divisors
 import Mathlib.NumberTheory.FrobeniusNumber