Commit 2025-09-02 03:14 714adfbd

View on Github →

chore: delete >6 month old Deprecated.Order (#29125)

Estimated changes

deleted theorem exists_square_le'
deleted theorem le_mul_of_le_of_one_le'
deleted theorem lt_mul_of_le_of_one_lt'
deleted theorem lt_mul_of_lt_of_one_le'
deleted theorem mul_le_of_le_of_le_one'
deleted theorem mul_le_of_le_one_of_le'
deleted theorem mul_lt_of_le_of_lt_one'
deleted theorem mul_lt_of_le_one_of_lt'
deleted theorem mul_lt_of_lt_of_le_one'
deleted theorem mul_lt_of_lt_one_of_le'