Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ring_char.eq

Modification history

2022-01-14 14:12
src/algebra/char_p/basic.lean
chore(algebra/char_p): ring_char.eq is better in the other direction, with instances, and explicit arguments (#11439)
Modified ring_char.eqView on Github →
2020-11-28 17:42
src/algebra/char_p/basic.lean
chore(algebra/char_p): refactor char_p (#5132)
Modified ring_char.eqView on Github →
2018-11-05 17:58
algebra/char_p.lean
feat(algebra/char_p): define the characteristic of a semiring
Added ring_char.eqView on Github →