Theorem split_by_characteristic

Modification history

2026-03-20 06:03

Mathlib/Algebra/CharP/MixedCharZero.lean

chore(Algebra/CharP/MixedCharZero): cleanup file and use module system (#34676) …

Modified split_by_characteristic View on Github →

2023-05-21 13:23

Mathlib/Algebra/CharP/MixedCharZero.lean

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

Added split_by_characteristic View on Github →