Commit 2025-11-24 09:57 cbda945d

View on Github →

chore: golf proofs that use 0 < x ↔ x ≠ 0 (#31895) This reduces the diff of #31749.

Estimated changes

Modified Mathlib/Algebra/Order/Field/Canonical.lean

Modified Mathlib/Analysis/ConstantSpeed.lean

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Function/UniformIntegrable.lean

Modified Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/VitaliCaratheodory.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

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

Modified Mathlib/MeasureTheory/Measure/MutuallySingular.lean

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

Modified Mathlib/MeasureTheory/Measure/Tight.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

modified theorem NumberField.mixedEmbedding.minkowskiBound_pos

Modified Mathlib/NumberTheory/WellApproximable.lean

Modified Mathlib/Probability/Kernel/Composition/Comp.lean

Modified Mathlib/Probability/Kernel/Defs.lean

Modified Mathlib/Probability/Kernel/Disintegration/Density.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Basic.lean

Modified Mathlib/Probability/Process/Kolmogorov.lean

Modified Mathlib/RingTheory/MvPowerSeries/LexOrder.lean

modified theorem MvPowerSeries.lexOrder_zero

Modified Mathlib/RingTheory/Valuation/Archimedean.lean

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

modified theorem Ordinal.nmul_zero

Modified Mathlib/SetTheory/Ordinal/Principal.lean

modified theorem Ordinal.principal_zero