Commit 2022-07-19 18:28 2ee2bae0

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.