Commit 2024-06-26 16:30 cabd7872
View on Github →feat(Data/Real/EReal): add theorems (#14125)
- Add
add_sub_cancel_right
- Add
right_distrib_of_nneg
- Add
left_distrib_of_nneg
- Add
le_iff_le_forall_real_gt
feat(Data/Real/EReal): add theorems (#14125)
add_sub_cancel_right
right_distrib_of_nneg
left_distrib_of_nneg
le_iff_le_forall_real_gt