Documentation

Mathlib.Tactic.ArithMult.Init

arith_mult Rule Set #

This module defines the IsMultiplicative Aesop rule set which is used by the arith_mult tactic. Aesop rule sets only become visible once the file in which they're declared is imported, so we must put this declaration into its own file.