mathlib
798024a9
- chore(data/real/*): rename `le_of_forall_epsilon_le` to `le_of_forall_pos_le_add` (#5761)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
5 years ago
chore(data/real/*): rename `le_of_forall_epsilon_le` to `le_of_forall_pos_le_add` (#5761) * generalize the `real` version to a `linear_ordered_add_comm_group`; * rename `nnreal` and `ennreal` versions.
Author
urkud
Parents
78493c9d
Loading