mathlib3
fix(tactic/ring): more precise pattern match for div
#1557

Merged

fix(tactic/ring): more precise pattern match for div #1557

mergify merged 13 commits into master from ring-div

robertylewis commented on 2019-10-16

robertylewis assigned

robertylewis 6 years ago

robertylewis added awaiting-author

digama0 removed awaiting-author

fpvandoorn added WIP

fix(tactic/ring): more precise pattern match for div

587a89ed

add test

076db0c2

fix instance check for div

84f16d8d

chore(algebra/quadratic_discriminant): add braces in have steps

c3f37fc9

use norm_num instead of ring to evaluate exponents

a3b12189

fix norm_num uses

50963ebf

fix norm_num pow bug

e6d0c71c

bugfix

300bbdc4

digama0 force pushed from b46a6b30 to 300bbdc4 6 years ago

Merge branch 'master' into ring-div

01c2893d

Merge remote-tracking branch 'blessed/master' into ring-div

f8501313

Merge branch 'master' into ring-div

bd598519

fix proof

48db96f7

robertylewis approved these changes on 2020-02-28

robertylewis removed WIP

robertylewis added ready-to-merge

Merge branch 'master' into ring-div

e3abf7a3

mergify merged 4149099c into master 6 years ago

mergify deleted the ring-div branch 6 years ago

bryangingechen added t-meta

Reviewers

robertylewis

ChrisHughes24

Assignees

robertylewis

Labels

ready-to-merge t-meta

Milestone

No milestone

mathlib3 fix(tactic/ring): more precise pattern match for div #1557 Merged

fix(tactic/ring): more precise pattern match for div #1557

mathlib3
fix(tactic/ring): more precise pattern match for div
#1557

Merged