Commit 2026-03-17 23:30 c0ae7a0c

View on Github →

feat: Nat/Int casts on char two rings (#34622)

Estimated changes

Modified Mathlib/Algebra/CharP/Two.lean

added theorem CharTwo.intCast_cases

added theorem CharTwo.intCast_eq_ite

added theorem CharTwo.intCast_eq_mod

added theorem CharTwo.natCast_cases

added theorem CharTwo.natCast_eq_ite

added theorem CharTwo.natCast_eq_mod

added theorem CharTwo.ofNat_eq_mod

added theorem CharTwo.range_intCast

added theorem CharTwo.range_natCast

modified theorem CharTwo.two_eq_zero

Modified Mathlib/Data/Set/Insert.lean

added theorem Set.range_ite_const