Ssreflect Users Discussion List

[Xavier Allamigeon <>]

Dear Cyril,

Le 23/05/2018 à 19:30, Cyril a écrit :
> The "right way" to do it is not to define a specific coercion
> (matR_of_matR') but use "map_mx inR" instead (where you may define inR :
> R' -> R to be val and prove it is a ring morphism). Then you can use
> raddf0, raddfD, raddf*... (because map_mx f is additive when f is), or
> theorems specific to map_mx such as map_mx1, map_mxZ, map_mxM, etc.
> (There is currently nothing like "piE" to use them all in one go).
Thanks for your detailed explanations!

Best,
Xavier