Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-09-02 03:14
714adfbd
View on Github →
chore: delete >6 month old
Deprecated.Order
(
#29125
)
Estimated changes
Modified
Mathlib.lean
Deleted
Mathlib/Deprecated/Order.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