mathlib documentation

algebra.char_zero

source
@[class]
structure char_zero (α : Type u_1) [add_monoid α] [has_one α] :
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 {α : Type u_1} [add_monoid α] [has_one α] (add_left_cancel : ∀ (a b c : α), a + b = a + c → b = c) (H : ∀ (n : ℕ), ↑n = 0 → n = 0) :
char_zero α

source
theorem add_group.char_zero_of_inj_zero {α : Type u_1} [add_group α] [has_one α] (H : ∀ (n : ℕ), ↑n = 0 → n = 0) :
char_zero α

source
theorem ordered_cancel_comm_monoid.char_zero_of_inj_zero {α : Type u_1} [ordered_cancel_add_comm_monoid α] [has_one α] (H : ∀ (n : ℕ), ↑n = 0 → n = 0) :
char_zero α

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

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

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

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

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

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

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

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

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

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

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

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

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

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