Commit 2023-03-23 13:32 59f1d8c2

View on Github →

feat: port Algebra.CharP.Algebra (#3037)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/CharP/Algebra.lean

added theorem Algebra.charP_iff

added theorem Algebra.ringChar_eq

added theorem IsFractionRing.charP_of_isFractionRing

added theorem IsFractionRing.charZero_of_isFractionRing

added theorem algebraRat.charP_zero

added theorem algebraRat.charZero

added theorem charP_of_injective_algebraMap'

added theorem charP_of_injective_algebraMap

added theorem charZero_of_injective_algebraMap