mathlib3

2ee2bae0 - chore({algebra,data/rat}): use forgetful inheritance for `algebra_rat` (#14894)

chore({algebra,data/rat}): use forgetful inheritance for `algebra_rat` (#14894) Throughout mathlib we've been struggling with diamonds arising from the `algebra_rat [division_ring K] [char_zero K] : algebra ℚ K` instance: since this instance provided its own inclusion map `to_fun : ℚ → K` and scalar multiplication by rationals `smul : ℚ → K → K`, it would not be definitionally equal to other instances such as `algebra.id`, and we'd need tactics like `convert` to deal with this inequality. Following the previous `nsmul` and `zmul` refactors, this PR applies the forgetful inheritance pattern to the `algebra_rat` instance, allowing you to supply a definitionally convenient value for the conflicting `to_fun` and `smul` fields as the fields `of_rat` and `qsmul` in the `division_ring K` instance. `of_rat` is used to define the coercion `ℚ → K` (in the instance `rat.cast_coe`), whic is used to define the map `rat.cast_hom : ℚ →+* K`, which is used along with `qsmul` to define `algebra_rat`. A default value for `of_rat` and `qsmul` and coherence proofs are provided using the `opt_param`/`auto_param` mechanism, just like for `nsmul` and `zsmul`. I have included a test after the definition of `algebra_rat`, to ensure definitional equality with `algebra.id`.