Injectivity of int.cast
into characteristic zero rings and fields. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[simp]
data.int.char_zero
int.cast
into characteristic zero rings and fields. #THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.