Commit 2022-12-10 13:29 26c48564

View on Github →

feat port: Algebra.Order.Group.MinMax (#933) 10b4e499f43088dd3bb7b5796184ad5216648ab1 A couple of times I had to explicitly give a Type to a lemma so Type class inference would work. No issues other than that

Estimated changes

added theorem abs_max_sub_max_le_abs
added theorem abs_max_sub_max_le_max
added theorem abs_min_sub_min_le_max
added theorem max_div_div_left'
added theorem max_div_div_right'
added theorem max_inv_inv'
added theorem max_sub_max_le_max
added theorem min_div_div_left'
added theorem min_div_div_right'
added theorem min_inv_inv'