Mathlib v3 is deprecated. Go to Mathlib v4

Theorem ring_hom.char_p_iff_char_p

Modification history

2021-08-21 15:59

src/algebra/char_p/basic.lean

feat(field_theory): finite fields exist (#8692)

Modified ring_hom.char_p_iff_char_p View on Github →

2020-10-13 11:12

src/algebra/char_p.lean

feat(algebra/char_p): fields with a hom between them have same char (#4594)

Added ring_hom.char_p_iff_char_p View on Github →