Commit 2023-12-26 07:50 23429eb2

View on Github →

feat: 0 ≤ a * b ↔ (0 < a → 0 ≤ b) ∧ (0 < b → 0 ≤ a) (#9219) I had a slightly logic-heavy argument that was nicely simplified by stating this lemma. Also fix a few lemma names. From LeanAPAP and LeanCamCombi

Estimated changes

Modified Mathlib/Algebra/Order/Floor.lean

Modified Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

modified theorem eq_one_or_one_lt

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

deleted theorem CanonicallyOrderedCommSemiring.mul_pos

added theorem add_sq_le

Modified Mathlib/Algebra/Order/Ring/Defs.lean

added theorem mul_nonneg_iff_neg_imp_nonpos

added theorem mul_nonneg_iff_of_pos_left

added theorem mul_nonneg_iff_of_pos_right

added theorem mul_nonneg_iff_pos_imp_nonneg

added theorem mul_nonpos_iff_neg_imp_nonneg

added theorem mul_nonpos_iff_pos_imp_nonpos

deleted theorem zero_le_mul_left

deleted theorem zero_le_mul_right

Modified Mathlib/Algebra/Order/Ring/Lemmas.lean

added theorem mul_pos_iff_of_pos_left

added theorem mul_pos_iff_of_pos_right

deleted theorem zero_lt_mul_left

deleted theorem zero_lt_mul_right

Modified Mathlib/Analysis/Hofer.lean

Modified Mathlib/Analysis/InnerProductSpace/Spectrum.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/Combinatorics/SimpleGraph/DegreeSum.lean

Modified Mathlib/Combinatorics/SimpleGraph/Regularity/Bound.lean

Modified Mathlib/MeasureTheory/Covering/LiminfLimsup.lean

Modified Mathlib/NumberTheory/DiophantineApproximation.lean

Modified Mathlib/NumberTheory/FLT/Four.lean

Modified Mathlib/NumberTheory/SumFourSquares.lean

Modified Mathlib/Probability/Distributions/Gaussian.lean

Modified Mathlib/Tactic/NormNum/Prime.lean