mathlib documentation

algebra.char_zero

source
@[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
source
theorem char_zero_of_inj_zero {R : Type u_1} [add_left_cancel_monoid R] [has_one R] :
(∀ (n : ℕ), ↑n = 0 → n = 0) → char_zero R

source
@[instance]
def linear_ordered_semiring.to_char_zero {R : Type u_1} [linear_ordered_semiring R] :
char_zero R

source
theorem nat.cast_injective {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] :
function.injective coe

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

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

source
theorem nat.cast_ne_zero {R : Type u_1} [add_monoid R] [has_one R] [char_zero R] {n : ℕ} :
↑n ≠ 0 ↔ n ≠ 0

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

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

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

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

source
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

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

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

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

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

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

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