mathlib3
0723536a - chore(data/zmod/algebra): make zmod.algebra a def (#19197)

Commit
2 years ago
chore(data/zmod/algebra): make zmod.algebra a def (#19197) `zmod.algebra` creates a diamond about the `zmod p`-algebra structure on `zmod p`: ```lean 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.
Parents
Loading