mathlib docs: algebra.char

@[class]

structure char_zero (α : Type u_1) [add_monoid α] [has_one α] :

Prop

cast_injective : function.injective coe

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 α] :

(∀ (a b c : α), a + b = a + c → b = c) → (∀ (n : ℕ), ↑n = 0 → n = 0) → char_zero α

source

theorem add_group.char_zero_of_inj_zero {α : Type u_1} [add_group α] [has_one α] :

(∀ (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 α] :

(∀ (n : ℕ), ↑n = 0 → n = 0) → char_zero α

source

@[instance]

def linear_ordered_semiring.to_char_zero {α : Type u_1} [linear_ordered_semiring α] :

char_zero α

Equations

linear_ordered_semiring.to_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 ∣ 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)

mathlib documentation

algebra.char_zero

General documentation

Additional documentation

Library

mathlib documentation

algebra.​char_zero

General documentation

Additional documentation

Library

algebra.char_zero