Mathlib v3 is deprecated. Go to Mathlib v4

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 a linear_ordered_add_comm_group;
  • rename nnreal and ennreal versions.

Estimated changes