Commit 2025-02-16 10:37 2c4bbc98

View on Github →

chore(Algebra/CharZero/Lemmas): split into Ring and Field parts (#21920) Move the Field lemmas earlier, move the Ring lemmas to a new file Algebra.Ring.CharZero. The CharZero instances for WithBot and WithTop duplicate existing ones in Mathlib.Algebra.Order.Monoid.Unbundled.WithTop.

Estimated changes

deleted theorem CharZero.eq_neg_self_iff
deleted theorem CharZero.neg_eq_self_iff
deleted theorem Function.support_natCast
deleted def Nat.castEmbedding
deleted theorem Nat.cast_div_charZero
deleted theorem Nat.cast_pow_eq_one
deleted theorem RingHom.charZero
deleted theorem RingHom.charZero_iff
deleted theorem RingHom.injective_nat
deleted theorem add_halves
deleted theorem add_self_div_two
deleted theorem add_self_eq_zero
deleted theorem half_sub
deleted theorem nat_mul_inj'
deleted theorem nat_mul_inj
deleted theorem neg_units_ne_self
deleted theorem sub_half
deleted theorem units_ne_neg_self
added theorem add_halves
added theorem add_self_div_two
added theorem half_sub
added theorem sub_half
added theorem Nat.cast_pow_eq_one
added theorem RingHom.charZero
added theorem RingHom.charZero_iff
added theorem RingHom.injective_nat
added theorem add_self_eq_zero
added theorem nat_mul_inj'
added theorem nat_mul_inj
added theorem neg_units_ne_self
added theorem units_ne_neg_self
modified theorem Nat.cast_div
added theorem Nat.cast_div_charZero