Commit 2026-02-09 08:58 39fa7ca7

View on Github →

feat: generalize Subfield.charP to DivisionRing (#34623) And also add a variable block while we're at it.

Estimated changes

Modified Mathlib/Algebra/CharP/Algebra.lean

modified theorem CharP.dvd_of_ringHom

modified theorem CharP.of_ringHom_of_ne_zero

modified theorem ExpChar.of_injective_algebraMap'

modified theorem RingHom.charP

modified theorem RingHom.expChar

modified theorem RingHom.expChar_iff

modified theorem charP_of_injective_algebraMap'

modified theorem charP_of_injective_algebraMap

modified theorem charP_of_injective_ringHom

modified theorem charZero_of_injective_algebraMap

modified theorem charZero_of_injective_ringHom

modified theorem expChar_of_injective_algebraMap

modified theorem expChar_of_injective_ringHom

Modified Mathlib/Algebra/CharP/IntermediateField.lean