I seem to recall that algebra tactics also work for stdlib rings/fields. However, rereading the documentation, this does not seem to be the case.

Am I misremembering? Is there another standard solution?

https://github.com/math-comp/algebra-tactics

I'm not sure I understand the question, algebra-tactics is for matchomp not for stdlib. You can still equip the stdlib types with mathcomp structures to get some compatibility but otherwise I don't think it's expected to work out of the box (some of these structures, for Z, may already exist in mczify though).

At least `ring`

and `field`

of Algebra Tactics provide a special treatment for `Z`

: https://github.com/math-comp/algebra-tactics/blob/master/theories/ring.elpi#L205 (If you read the paper, I guess this is what you "misremember.")

You can embed `Z`

to any ring through the `int_of_Z`

morphism and `_%:~R`

. Algebra Tactics can recognize these morphisms.

Thanks. Yes, I was thinking of some mczify type of preprocessing.

Last updated: Jul 15 2024 at 20:02 UTC