← Mathematical handbook

def Lean.Grind.CommRing.Power.renameVars (pw : Power) (f : Meta.Grind.VarRename) : Power

Equations

• pw.renameVars f = { x := (fun (x : Lean.Meta.Grind.Var) => f.map[x]?.getD 0) pw.x, k := pw.k }

def Lean.Grind.CommRing.Mon.renameVars (m : Mon) (f : Meta.Grind.VarRename) : Mon

Equations

• Lean.Grind.CommRing.Mon.unit.renameVars f = Lean.Grind.CommRing.Mon.unit
• (Lean.Grind.CommRing.Mon.mult pw m_2).renameVars f = Lean.Grind.CommRing.Mon.mult (pw.renameVars f) (m_2.renameVars f)

def Lean.Grind.CommRing.Poly.renameVars (p : Poly) (f : Meta.Grind.VarRename) : Poly

Equations

• (Lean.Grind.CommRing.Poly.num k).renameVars f = Lean.Grind.CommRing.Poly.num k
• (Lean.Grind.CommRing.Poly.add k m p_2).renameVars f = Lean.Grind.CommRing.Poly.add k (m.renameVars f) (p_2.renameVars f)

def Lean.Grind.CommRing.Expr.renameVars (e : Expr) (f : Meta.Grind.VarRename) : Expr

Equations

• (Lean.Grind.CommRing.Expr.num k).renameVars f = Lean.Grind.CommRing.Expr.num k
• (Lean.Grind.CommRing.Expr.natCast k).renameVars f = Lean.Grind.CommRing.Expr.natCast k
• (Lean.Grind.CommRing.Expr.intCast k).renameVars f = Lean.Grind.CommRing.Expr.intCast k
• (Lean.Grind.CommRing.Expr.var x).renameVars f = Lean.Grind.CommRing.Expr.var ((fun (x : Lean.Meta.Grind.Var) => f.map[x]?.getD 0) x)
• a.neg.renameVars f = (a.renameVars f).neg
• (a.add b).renameVars f = (a.renameVars f).add (b.renameVars f)
• (a.sub b).renameVars f = (a.renameVars f).sub (b.renameVars f)
• (a.mul b).renameVars f = (a.renameVars f).mul (b.renameVars f)
• (a.pow k).renameVars f = (a.renameVars f).pow k

def Lean.Grind.CommRing.Power.collectVars (pw : Power) : Meta.Grind.VarCollector

Equations

• pw.collectVars = Lean.Meta.Grind.collectVar pw.x

def Lean.Grind.CommRing.Mon.collectVars (m : Mon) : Meta.Grind.VarCollector

Equations

• Lean.Grind.CommRing.Mon.unit.collectVars = id
• (Lean.Grind.CommRing.Mon.mult pw m_2).collectVars = pw.collectVars >> m_2.collectVars

def Lean.Grind.CommRing.Poly.collectVars (p : Poly) : Meta.Grind.VarCollector

Equations

• (Lean.Grind.CommRing.Poly.num k).collectVars = id
• (Lean.Grind.CommRing.Poly.add k m p_2).collectVars = m.collectVars >> p_2.collectVars

def Lean.Grind.CommRing.Expr.collectVars (e : Expr) : Meta.Grind.VarCollector

Equations

• (Lean.Grind.CommRing.Expr.num k).collectVars = id
• (Lean.Grind.CommRing.Expr.natCast k).collectVars = id
• (Lean.Grind.CommRing.Expr.intCast k).collectVars = id
• (Lean.Grind.CommRing.Expr.var x).collectVars = Lean.Meta.Grind.collectVar x
• a.neg.collectVars = a.collectVars
• (a.pow k).collectVars = a.collectVars
• (a.add b).collectVars = a.collectVars >> b.collectVars
• (a.sub b).collectVars = a.collectVars >> b.collectVars
• (a.mul b).collectVars = a.collectVars >> b.collectVars