mathlib
b9e3dbba - feat(rat): give Q-algebra structure on field (#1628)

Commit

6 years ago

feat(rat): give Q-algebra structure on field (#1628) also move around some declarations in rat.cast the only new declaration in that file is is_ring_hom_cast

References

#1628 - feat(rat): give Q-algebra structure on field

Author

fpvandoorn

Committer

mergify[bot]

Parents

b5b674c2

mathlib b9e3dbba - feat(rat): give Q-algebra structure on field (#1628)

mathlib
b9e3dbba - feat(rat): give Q-algebra structure on field (#1628)