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_rightright_distrib_of_nnegleft_distrib_of_nnegle_iff_le_forall_real_gt