Documentation

Mathlib.Tactic.Algebra.AlgebraNF

The algebra_nf tactic #

This file contains helper functions for the (currently unimplemented) algebra_nf tactic.

The defnitions in this file are currently only used by polynomial_nf.

source
def Mathlib.Tactic.Algebra.cleanupSMul (cfg : RingNF.Config) (r : Lean.Meta.Simp.Result) :
Lean.MetaM Lean.Meta.Simp.Result

Clean up the normal form into a more human-friendly format. This does everything RingNF.cleanup does and also pulls the scalar multiplication from the end of of each term to the start. i.e. x * y * (r • 1) → r • (x * y) Used by cleanup.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Mathlib.Tactic.Algebra.cleanupConsts (cfg : RingNF.Config) (r : Lean.Meta.Simp.Result) :
    Lean.MetaM Lean.Meta.Simp.Result

    Turn scalar multiplication by an explicit constant in R into multiplication in A.

    e.g. (4 : ℚ) • x becomes 4 * x but ↑n • x stays ↑n • x.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Mathlib.Tactic.Algebra.evalExpr {u : Lean.Level} (R : Q(Type u)) (e : Lean.Expr) :
      AtomM Lean.Meta.Simp.Result

      The core of algebra_nf with R - normalize the expression e over the base ring R Also used internally in polynomial_nf.

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