mathlib

3a714995 - feat(ring_theory/algebra) : generalize `rat.algebra_rat` to `division_ring` (#2208)

feat(ring_theory/algebra) : generalize `rat.algebra_rat` to `division_ring` (#2208) Other changes: * add lemmas about field inverse to `algebra/semiconj` and `algebra/commute`; * drop `rat.cast`, define `instance : has_coe` right away to avoid accidental use of `rat.cast` in theorems; * define `rat.cast_hom` instead of `is_ring_hom rat.cast`; * generalize some theorems about from `field` to `division_ring`. Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>