Documentation

Mathlib.Tactic.NormNum.Inv

norm_num plugins for Rat.cast and ⁻¹. #

The norm_num extension which identifies expressions of the form mkRat a b, such that norm_num successfully recognises both a and b, and returns a / b.

Instances For

    The norm_num extension which identifies an expression RatCast.ratCast q where norm_num recognizes q, returning the cast of q.

    Instances For

      The norm_num extension which identifies expressions of the form a⁻¹, such that norm_num successfully recognises a.

      Instances For