Commit 2023-05-21 13:23 ab900bdd

View on Github →

feat: port Algebra.CharP.MixedCharZero (#3222)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/CharP/MixedCharZero.lean

added theorem EqualCharZero.PNat.isUnit_natCast

added theorem EqualCharZero.iff_not_mixedCharZero

added theorem EqualCharZero.nonempty_algebraRat_iff

added theorem EqualCharZero.of_algebraRat

added theorem EqualCharZero.of_not_mixedCharZero

added theorem EqualCharZero.pnatCast_eq_natCast

added theorem EqualCharZero.pnatCast_one

added theorem EqualCharZero.to_not_mixedCharZero

added theorem MixedCharZero.reduce_to_maximal_ideal

added theorem MixedCharZero.reduce_to_p_prime

added theorem isEmpty_algebraRat_iff_mixedCharZero

added theorem split_by_characteristic

added theorem split_by_characteristic_domain

added theorem split_by_characteristic_localRing

added theorem split_equalCharZero_mixedCharZero

Modified Mathlib/Algebra/Group/Units.lean

modified theorem Units.ext