mathlib
4149099c - fix(tactic/ring): more precise pattern match for div (#1557)

Commit
6 years ago
fix(tactic/ring): more precise pattern match for div (#1557) * fix(tactic/ring): more precise pattern match for div * add test * fix instance check for div * chore(algebra/quadratic_discriminant): add braces in have steps * use norm_num instead of ring to evaluate exponents * fix norm_num uses * fix norm_num pow bug * bugfix * fix proof Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading