Commit 2023-06-19 20:03 0723536a

chore(data/zmod/algebra): make zmod.algebra a def (#19197) zmod.algebra creates a diamond about the zmod p-algebra structure on zmod p:

import algebra.algebra.basic
import data.zmod.algebra
example (p : ℕ) : algebra.id (zmod p) =
  (zmod.algebra (zmod p) p) := rfl --fails

This is also causing troubles with the port. We turn zmod.algebra into a def.