Commit 2021-03-10 17:05 f675a864
View on Github →feat(data/real/{nnreal,ennreal}): add (e)nnreal.of_real_bit0/bit1 (#6617)
Add bit0/bit1 lemmas for nnreal.of_real, ennreal.of_real and ennreal.to_nnreal.
With these additions, it is for example possible to prove h : ennreal.of_real (2 : ℝ) = 2 := by simp.