Def Mathlib.Tactic.Rify.mkRifyContext

Modification history

2026-02-22 22:01

Mathlib/Tactic/Rify.lean

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

Added Mathlib.Tactic.Rify.mkRifyContext View on Github →