Commit 2025-04-06 19:13 d66533d9

View on Github →

chore: move deprecated lemmas in Algebra.Order.GroupWithZero.Unbundled (#23731) …to Deprecated.Order. Split from #23620.

Estimated changes

Modified Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

deleted theorem Left.lt_mul_of_lt_of_one_le_of_nonneg

deleted theorem Left.mul_le_one_of_le_of_le

deleted theorem Left.mul_lt_of_le_of_lt_one_of_pos

deleted theorem Left.mul_lt_of_lt_of_le_one_of_nonneg

deleted theorem Left.one_le_mul_of_le_of_le

deleted theorem Left.one_lt_mul_of_le_of_lt_of_pos

deleted theorem Right.mul_le_one_of_le_of_le

deleted theorem Right.mul_lt_one_of_le_of_lt_of_nonneg

deleted theorem Right.mul_lt_one_of_lt_of_le_of_pos

deleted theorem Right.one_le_mul_of_le_of_le

deleted theorem Right.one_lt_mul_of_le_of_lt_of_nonneg

deleted theorem Right.one_lt_mul_of_lt_of_le_of_pos

deleted theorem Right.one_lt_mul_of_lt_of_lt

deleted theorem exists_square_le'

deleted theorem le_mul_of_le_of_one_le'

deleted theorem le_mul_of_le_of_one_le_of_nonneg

deleted theorem le_mul_of_one_le_of_le_of_nonneg

deleted theorem le_of_le_mul_of_le_one_of_nonneg_left

deleted theorem le_of_le_mul_of_le_one_of_nonneg_right

deleted theorem le_of_mul_le_of_one_le_nonneg_right

deleted theorem le_of_mul_le_of_one_le_of_nonneg_left

deleted theorem lt_mul_of_le_of_one_lt'

deleted theorem lt_mul_of_le_of_one_lt_of_pos

deleted theorem lt_mul_of_lt_of_one_le'

deleted theorem lt_mul_of_lt_of_one_le_of_nonneg

deleted theorem lt_mul_of_lt_of_one_lt_of_pos

deleted theorem lt_mul_of_one_le_of_lt_of_nonneg

deleted theorem lt_mul_of_one_lt_of_le_of_pos

deleted theorem lt_mul_of_one_lt_of_lt_of_nonneg

deleted theorem lt_mul_of_one_lt_of_lt_of_pos

deleted theorem lt_of_lt_mul_of_le_one_of_nonneg_left

deleted theorem lt_of_lt_mul_of_le_one_of_nonneg_right

deleted theorem lt_of_mul_lt_of_one_le_of_nonneg_left

deleted theorem mul_le_of_le_of_le_one'

deleted theorem mul_le_of_le_of_le_one_of_nonneg

deleted theorem mul_le_of_le_one_of_le'

deleted theorem mul_le_of_le_one_of_le_of_nonneg

deleted theorem mul_lt_of_le_of_lt_one'

deleted theorem mul_lt_of_le_of_lt_one_of_pos

deleted theorem mul_lt_of_le_one_of_lt'

deleted theorem mul_lt_of_le_one_of_lt_of_nonneg

deleted theorem mul_lt_of_lt_of_le_one'

deleted theorem mul_lt_of_lt_of_le_one_of_nonneg

deleted theorem mul_lt_of_lt_of_lt_one_of_pos

deleted theorem mul_lt_of_lt_one_of_le'

deleted theorem mul_lt_of_lt_one_of_le_of_pos

deleted theorem mul_lt_of_lt_one_of_lt_of_pos

Modified Mathlib/Deprecated/Order.lean

added theorem Left.lt_mul_of_lt_of_one_le_of_nonneg

added theorem Left.mul_le_one_of_le_of_le

added theorem Left.mul_lt_of_le_of_lt_one_of_pos

added theorem Left.mul_lt_of_lt_of_le_one_of_nonneg

added theorem Left.one_le_mul_of_le_of_le

added theorem Left.one_lt_mul_of_le_of_lt_of_pos

added theorem Right.mul_le_one_of_le_of_le

added theorem Right.mul_lt_one_of_le_of_lt_of_nonneg

added theorem Right.mul_lt_one_of_lt_of_le_of_pos

added theorem Right.one_le_mul_of_le_of_le

added theorem Right.one_lt_mul_of_le_of_lt_of_nonneg

added theorem Right.one_lt_mul_of_lt_of_le_of_pos

added theorem Right.one_lt_mul_of_lt_of_lt

added theorem exists_square_le'

added theorem le_mul_of_le_of_one_le'

added theorem le_mul_of_le_of_one_le_of_nonneg

added theorem le_mul_of_one_le_of_le_of_nonneg

added theorem le_of_le_mul_of_le_one_of_nonneg_left

added theorem le_of_le_mul_of_le_one_of_nonneg_right

added theorem le_of_mul_le_of_one_le_nonneg_right

added theorem le_of_mul_le_of_one_le_of_nonneg_left

added theorem lt_mul_of_le_of_one_lt'

added theorem lt_mul_of_le_of_one_lt_of_pos

added theorem lt_mul_of_lt_of_one_le'

added theorem lt_mul_of_lt_of_one_le_of_nonneg

added theorem lt_mul_of_lt_of_one_lt_of_pos

added theorem lt_mul_of_one_le_of_lt_of_nonneg

added theorem lt_mul_of_one_lt_of_le_of_pos

added theorem lt_mul_of_one_lt_of_lt_of_nonneg

added theorem lt_mul_of_one_lt_of_lt_of_pos

added theorem lt_of_lt_mul_of_le_one_of_nonneg_left

added theorem lt_of_lt_mul_of_le_one_of_nonneg_right

added theorem lt_of_mul_lt_of_one_le_of_nonneg_left

added theorem mul_le_of_le_of_le_one'

added theorem mul_le_of_le_of_le_one_of_nonneg

added theorem mul_le_of_le_one_of_le'

added theorem mul_le_of_le_one_of_le_of_nonneg

added theorem mul_lt_of_le_of_lt_one'

added theorem mul_lt_of_le_of_lt_one_of_pos

added theorem mul_lt_of_le_one_of_lt'

added theorem mul_lt_of_le_one_of_lt_of_nonneg

added theorem mul_lt_of_lt_of_le_one'

added theorem mul_lt_of_lt_of_le_one_of_nonneg

added theorem mul_lt_of_lt_of_lt_one_of_pos

added theorem mul_lt_of_lt_one_of_le'

added theorem mul_lt_of_lt_one_of_le_of_pos

added theorem mul_lt_of_lt_one_of_lt_of_pos