basic): the characteristic is the order of one and zmod related lemmas (#16277)

Commit

3 years ago

feat(algebra/char_p/basic + data/zmod/basic): the characteristic is the order of one and zmod related lemmas (#16277) [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F)

Author

adomani

Parents

8ad70779

mathlib3 e4b9af26 - feat(algebra/char_p/basic + data/zmod/basic): the characteristic is the order of one and zmod related lemmas (#16277)

mathlib3
e4b9af26 - feat(algebra/char_p/basic + data/zmod/basic): the characteristic is the order of one and zmod related lemmas (#16277)