Mathlib v3 is deprecated. Go to Mathlib v4

Theorem real.to_nnreal_pow

Modification history

2022-10-10 13:36
src/data/real/nnreal.lean
feat(measure_theory/measure/haar_lebesgue): the Lebesgue measure is doubling (#16885) …
Added real.to_nnreal_powView on Github →