Theorem NNReal.inv_mk

Modification history

2026-04-13 12:57

Mathlib/Data/NNReal/Defs.lean

style: fix whitespace (#37993) …

Modified NNReal.inv_mk View on Github →

2026-04-04 20:14

Mathlib/Data/NNReal/Defs.lean

feat: use a constructor for NNReal (#37609) …

Added NNReal.inv_mk View on Github →