zmod algebra diamond

Stream: maths

[Chris Hughes]

I found a diamond sadly

import data.zmod.algebra
import ring_theory.mv_polynomial.basic

example {p : ℕ} (σ : Type) : @mv_polynomial.algebra (zmod p) (zmod p) σ _ _ _ =
  zmod.algebra (mv_polynomial σ (zmod p)) p := rfl --doesn't work

Is there something we can do about this? Did we do something to fix this for int?

[Chris Hughes]

Maybe the map from zmod p needs to be part of the char_p typeclass. I am a little uncomfortable with how far we're taking the algebra type class and relying on type class inference to find all our ring homs we want to use.

[Eric Wieser]

Chris Hughes said:

Did we do something to fix this for int?

No, there was a slide in my FMM2021 talk about what we could do, but it hasn't been done