Commit 2023-09-07 12:30 23ffa510

View on Github →

chore: tidy various files (#7009)

Estimated changes

Modified Counterexamples/Monic_nonRegular.lean

Modified Mathlib/Algebra/Algebra/Basic.lean

Modified Mathlib/Algebra/Algebra/Opposite.lean

Modified Mathlib/Algebra/Free.lean

Modified Mathlib/Analysis/Calculus/Inverse.lean

Modified Mathlib/Analysis/InnerProductSpace/Orientation.lean

Modified Mathlib/Data/Part.lean

Modified Mathlib/Data/Seq/Computation.lean

Modified Mathlib/Data/Seq/WSeq.lean

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/Instances/Sphere.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

deleted theorem QuadraticForm.posDefOfNonneg

added theorem QuadraticForm.posDef_of_nonneg

Modified Mathlib/Logic/IsEmpty.lean

Modified Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean

deleted theorem MeasureTheory.TendstoInMeasure.aeMeasurable

added theorem MeasureTheory.TendstoInMeasure.aemeasurable

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

Modified Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean

Modified Mathlib/Probability/Independence/Kernel.lean

Modified Mathlib/Tactic/HaveI.lean

Modified Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean

Modified Mathlib/Topology/ExtremallyDisconnected.lean

deleted theorem ExtremallyDisconnected.disjoint_closure_of_disjoint_IsOpen

added theorem ExtremallyDisconnected.disjoint_closure_of_disjoint_isOpen

Modified Mathlib/Topology/Homotopy/HSpaces.lean

Modified docs/Conv/Guide.lean