Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-21 21:22 6f316375

View on Github →

refactor(analysis/nnreal): split up into data.real and analysis part

Estimated changes

Modified analysis/nnreal.lean

deleted theorem nnreal.sum_coe

deleted def nnreal

Created data/real/nnreal.lean

added theorem nnreal.sum_coe

added def nnreal