Commit 2023-07-13 08:07 6a00552b

View on Github →

chore: tidy various files (#5840)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

added theorem AlgebraicGeometry.QuasiSeparated.openCover_TFAE

deleted theorem AlgebraicGeometry.QuasiSeparated.openCover_tFAE

Modified Mathlib/Analysis/Calculus/ParametricIntegral.lean

Modified Mathlib/CategoryTheory/Sites/Coherent.lean

Modified Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

Modified Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

modified theorem Basis.addHaar_self

added theorem Basis.coe_parallelepiped

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

Modified Mathlib/ModelTheory/DirectLimit.lean

added theorem FirstOrder.Language.DirectedSystem.coe_natLERec

deleted theorem FirstOrder.Language.DirectedSystem.coe_natLeRec

added def FirstOrder.Language.DirectedSystem.natLERec

deleted def FirstOrder.Language.DirectedSystem.natLeRec

Modified Mathlib/ModelTheory/Fraisse.lean

Modified Mathlib/NumberTheory/LegendreSymbol/GaussSum.lean

Modified Mathlib/RingTheory/Nullstellensatz.lean

Modified Mathlib/Topology/ContinuousFunction/Sigma.lean