mathlib documentation

algebra.char_zero

@[class]
structure char_zero (R : Type u_1) [add_monoid R] [has_one R] :
Prop

Typeclass for monoids with characteristic zero. (This is usually stated on fields but it makes sense for any additive monoid with 1.)

Instances
theorem char_zero_of_inj_zero {R : Type u_1} [add_left_cancel_monoid R] [has_one R] :
(∀ (n : ), n = 0n = 0)char_zero R

@[simp]
theorem nat.cast_inj {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] {m n : } :
m = n m = n

@[simp]
theorem nat.cast_eq_zero {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] {n : } :
n = 0 n = 0

theorem nat.cast_ne_zero {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] {n : } :
n 0 n 0

theorem nat.cast_add_one_ne_zero {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] (n : ) :
n + 1 0

@[simp]
theorem nat.cast_dvd_char_zero {k : Type u_1} [field k] [char_zero k] {m n : } :
n m(m / n) = m / n

@[instance]
def char_zero.infinite (α : Type u_1) [add_monoid α] [has_one α] [char_zero α] :

theorem two_ne_zero' {α : Type u_1} [add_monoid α] [has_one α] [char_zero α] :
2 0

theorem add_self_eq_zero {R : Type u_1} [semiring R] [no_zero_divisors R] [char_zero R] {a : R} :
a + a = 0 a = 0

theorem bit0_eq_zero {R : Type u_1} [semiring R] [no_zero_divisors R] [char_zero R] {a : R} :
bit0 a = 0 a = 0

@[simp]
theorem half_add_self {R : Type u_1} [division_ring R] [char_zero R] (a : R) :
(a + a) / 2 = a

@[simp]
theorem add_halves' {R : Type u_1} [division_ring R] [char_zero R] (a : R) :
a / 2 + a / 2 = a

theorem sub_half {R : Type u_1} [division_ring R] [char_zero R] (a : R) :
a - a / 2 = a / 2

theorem half_sub {R : Type u_1} [division_ring R] [char_zero R] (a : R) :
a / 2 - a = -(a / 2)

@[instance]
def with_top.char_zero {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] :