Commit 2024-11-19 19:36 29f545b8

View on Github →

chore: generalise div_le_div to groups with zero (#18917) ... and lemmas around

Estimated changes

modified theorem div_le_div
modified theorem div_le_div_iff
deleted theorem div_le_div_of_nonneg_left
modified theorem div_le_div_right
modified theorem div_lt_div_iff
modified theorem div_lt_div_left
deleted theorem div_lt_div_of_pos_left
deleted theorem div_lt_div_of_pos_right
modified theorem div_lt_div_right
added theorem div_le_div_iff₀
modified theorem div_le_div₀
added theorem div_lt_div_iff₀
added theorem div_lt_div_of_pos_left
added theorem div_lt_div₀'
added theorem div_lt_div₀