def Lean.Meta.Grind.Arith.expandPowAdd : Simp.Simproc

Applies a^(m+n) = a^m * a^n, a^0 = 1, a^1 = a.

We do normalize a^0 and a^1 when converting expressions into polynomials, but we need to normalize them here when for other preprocessing steps such as a / b = a*b⁻¹. If b is of the form c^1, it will be treated as an atom in the comm ring module.

Equations

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

def Lean.Meta.Grind.Arith.addSimproc (s : Simprocs) : CoreM Simprocs

Equations

• Lean.Meta.Grind.Arith.addSimproc s = s.add `Lean.Meta.Grind.Arith.expandPowAdd true