Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-24 09:54 a21fcfad

View on Github →

feat(data/real/nnreal): upgrade nnabs to a monoid_with_zero_hom (#8844) Other changes:

  • add nnreal.finset_sup_div;
  • rename nnreal.coe_nnabs to real.coe_nnabs;
  • add real.nndist_eq and real.nndist_eq'.

Estimated changes

deleted theorem nnreal.coe_nnabs
added theorem nnreal.finset_sup_div
added theorem real.coe_nnabs
modified theorem real.coe_to_nnreal_le
modified def real.nnabs
modified theorem real.nnabs_of_nonneg
added theorem real.nndist_eq'
added theorem real.nndist_eq