Documentation

Mathlib.Tactic.NormNum

Imports

Init
Mathlib.Tactic.NormNum.Basic
Mathlib.Tactic.NormNum.DivMod
Mathlib.Tactic.NormNum.Eq
Mathlib.Tactic.NormNum.Ineq
Mathlib.Tactic.NormNum.Inv
Mathlib.Tactic.NormNum.OfScientific
Mathlib.Tactic.NormNum.Pow
Mathlib.Data.Rat.Cast.Order

Imported by

We register norm_num with the hint tactic.