Commit 2024-07-25 07:50 ec270f5b

View on Github →

chore(Algebra/Order/GroupWithZero/Unbundled): resolving name inconsistencies (#9904) This PR allows the names to be clearly distinguished from versions that do not require positivity assumptions, but also become too long. Due to name conflicts, some similar lemmas have dissimilar names before this PR:

theorem mul_lt_mul_of_nonneg_of_pos [PosMulMono α] [MulPosStrictMono α]
    (h₁ : a < b) (h₂ : c ≤ d) (a0 : 0 ≤ a) (d0 : 0 < d) : a * c < b * d
theorem mul_lt_mul_of_le_of_lt' [PosMulMono α] [MulPosStrictMono α]
    (h₁ : a < b) (h₂ : c ≤ d) (b0 : 0 ≤ b) (c0 : 0 < c) : a * c < b * d

| Statement | New name | Old name | |

Estimated changes

modified theorem Left.neg_of_mul_neg_left
modified theorem Left.neg_of_mul_neg_right
modified theorem Right.neg_of_mul_neg_left
modified theorem Right.neg_of_mul_neg_right
deleted theorem mul_le_mul
deleted theorem mul_le_mul_of_le_of_le
added theorem mul_le_mul_of_nonneg'
added theorem mul_le_mul_of_nonneg
deleted theorem mul_lt_mul_of_le_of_le'
deleted theorem mul_lt_mul_of_le_of_lt'
deleted theorem mul_lt_mul_of_lt_of_lt'
added theorem mul_lt_mul_of_pos'
added theorem mul_lt_mul_of_pos
deleted theorem mul_lt_mul_of_pos_of_pos
deleted theorem mul_lt_mul''
deleted theorem mul_lt_mul'
deleted theorem mul_lt_mul
deleted theorem neg_of_mul_neg_left
deleted theorem neg_of_mul_neg_right