Commit 2021-01-16 03:57 798024a9
View on Github →chore(data/real/*): rename le_of_forall_epsilon_le
to le_of_forall_pos_le_add
(#5761)
- generalize the
real
version to alinear_ordered_add_comm_group
; - rename
nnreal
andennreal
versions.
chore(data/real/*): rename le_of_forall_epsilon_le
to le_of_forall_pos_le_add
(#5761)
real
version to a linear_ordered_add_comm_group
;nnreal
and ennreal
versions.