Documentation

Lean.Meta.Tactic.Grind.Arith.Linear.Den

source
def Lean.Meta.Grind.Arith.Linear.RingIneqCnstr.cleanupDenominators (c : RingIneqCnstr) :
LinearM RingIneqCnstr
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Lean.Meta.Grind.Arith.Linear.RingEqCnstr.cleanupDenominators (c : RingEqCnstr) :
    LinearM RingEqCnstr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr.cleanupDenominators (c : RingDiseqCnstr) :
      LinearM RingDiseqCnstr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For