Documentation

Mathlib.Tactic.NormNum.Inv

norm_num plugins for Rat.cast and ⁻¹. #

Helper function to synthesize a typed CharZero α expression given Ring α.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Helper function to synthesize a typed CharZero α expression given Ring α, if it exists.

    Equations
    Instances For

      Helper function to synthesize a typed CharZero α expression given AddMonoidWithOne α.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Helper function to synthesize a typed CharZero α expression given AddMonoidWithOne α, if it exists.

        Equations
        Instances For

          Helper function to synthesize a typed CharZero α expression given DivisionRing α.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Helper function to synthesize a typed CharZero α expression given DivisionRing α, if it exists.

            Equations
            Instances For

              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.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

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

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    def Mathlib.Meta.NormNum.evalInv.core {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) (a : Q(«$α»)) (ra : Mathlib.Meta.NormNum.Result a) (dα : Q(DivisionRing «$α»)) (i : Option Q(CharZero «$α»)) :

                    Main part of evalInv.

                    Instances For