Def Mathlib.Tactic.Linarith.nnrealToReal

Modification history

2026-02-22 22:01

Mathlib/Tactic/Linarith/Preprocessing.lean

feat(Tactic): `linarith` and `rify` for NNReal (#35155)

Added Mathlib.Tactic.Linarith.nnrealToReal View on Github →