mathlib
3d60e134 - chore(algebra/field): move some lemmas from `field` to `division_ring` (#2331)

Commit

5 years ago

chore(algebra/field): move some lemmas from `field` to `division_ring` (#2331) Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

References

#2331 - chore(algebra/field): move some lemmas from `field` to `division_ring`

Author

urkud

Parents

a2e76391

mathlib 3d60e134 - chore(algebra/field): move some lemmas from `field` to `division_ring` (#2331)

mathlib
3d60e134 - chore(algebra/field): move some lemmas from `field` to `division_ring` (#2331)