Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-05 11:05 bb4099b4

View on Github →

feat(analysis/normed/normed_field): add abs_le_floor_nnreal_iff (#13130) From LTE.

Estimated changes