algebra.ring.defs - mathlib3 docs

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), non_unital_non_assoc_semiring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), non_unital_non_assoc_semiring.nsmul n.succ x = x + non_unital_non_assoc_semiring.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0

A not-necessarily-unital, not-necessarily-associative semiring.

Instances of this typeclass

Instances of other typeclasses for non_unital_non_assoc_semiring

non_unital_non_assoc_semiring.has_sizeof_inst

source

@[instance]

def non_unital_semiring.to_semigroup_with_zero (α : Type u) [self : non_unital_semiring α] :

semigroup_with_zero α

source

@[instance]

def non_unital_semiring.to_non_unital_non_assoc_semiring (α : Type u) [self : non_unital_semiring α] :

non_unital_non_assoc_semiring α

source

@[class]

structure non_unital_semiring (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), non_unital_semiring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), non_unital_semiring.nsmul n.succ x = x + non_unital_semiring.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)

An associative but not-necessarily unital semiring.

Instances of this typeclass

Instances of other typeclasses for non_unital_semiring

non_unital_semiring.has_sizeof_inst

source

@[instance]

def non_assoc_semiring.to_non_unital_non_assoc_semiring (α : Type u) [self : non_assoc_semiring α] :

non_unital_non_assoc_semiring α

source

@[instance]

def non_assoc_semiring.to_mul_zero_one_class (α : Type u) [self : non_assoc_semiring α] :

mul_zero_one_class α

source

@[instance]

def non_assoc_semiring.to_add_comm_monoid_with_one (α : Type u) [self : non_assoc_semiring α] :

add_comm_monoid_with_one α

source

@[class]

structure non_assoc_semiring (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), non_assoc_semiring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), non_assoc_semiring.nsmul n.succ x = x + non_assoc_semiring.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
nat_cast : ℕ → α
nat_cast_zero : non_assoc_semiring.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), non_assoc_semiring.nat_cast (n + 1) = non_assoc_semiring.nat_cast n + 1) . "control_laws_tac"

A unital but not-necessarily-associative semiring.

Instances of this typeclass

Instances of other typeclasses for non_assoc_semiring

non_assoc_semiring.has_sizeof_inst

source

@[instance]

def semiring.to_non_assoc_semiring (α : Type u) [self : semiring α] :

non_assoc_semiring α

source

@[class]

structure semiring (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), semiring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), semiring.nsmul n.succ x = x + semiring.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
nat_cast : ℕ → α
nat_cast_zero : semiring.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), semiring.nat_cast (n + 1) = semiring.nat_cast n + 1) . "control_laws_tac"
npow : ℕ → α → α
npow_zero' : (∀ (x : α), semiring.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), semiring.npow n.succ x = x * semiring.npow n x) . "try_refl_tac"

A semiring is a type with the following structures: additive commutative monoid (add_comm_monoid), multiplicative monoid (monoid), distributive laws (distrib), and multiplication by zero law (mul_zero_class). The actual definition extends monoid_with_zero instead of monoid and mul_zero_class.

Instances of this typeclass

Instances of other typeclasses for semiring

semiring.has_sizeof_inst

source

@[instance]

def semiring.to_non_unital_semiring (α : Type u) [self : semiring α] :

non_unital_semiring α

source

@[instance]

def semiring.to_monoid_with_zero (α : Type u) [self : semiring α] :

monoid_with_zero α

source

theorem one_add_one_eq_two {α : Type u} [has_one α] [has_add α] :

1 + 1 = 2

source

theorem add_one_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (a b : α) :

(a + 1) * b = a * b + b

source

theorem mul_add_one {α : Type u} [has_add α] [mul_one_class α] [left_distrib_class α] (a b : α) :

a * (b + 1) = a * b + a

source

theorem one_add_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (a b : α) :

(1 + a) * b = b + a * b

source

theorem mul_one_add {α : Type u} [has_add α] [mul_one_class α] [left_distrib_class α] (a b : α) :

a * (1 + b) = a + a * b

source

theorem two_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (n : α) :

2 * n = n + n

source

theorem bit0_eq_two_mul {α : Type u} [has_add α] [mul_one_class α] [right_distrib_class α] (n : α) :

bit0 n = 2 * n

source

theorem mul_two {α : Type u} [has_add α] [mul_one_class α] [left_distrib_class α] (n : α) :

n * 2 = n + n

source

theorem add_ite {α : Type u_1} [has_add α] (P : Prop) [decidable P] (a b c : α) :

a + ite P b c = ite P (a + b) (a + c)

source

@[simp]

theorem mul_ite {α : Type u_1} [has_mul α] (P : Prop) [decidable P] (a b c : α) :

a * ite P b c = ite P (a * b) (a * c)

source

theorem ite_add {α : Type u_1} [has_add α] (P : Prop) [decidable P] (a b c : α) :

ite P a b + c = ite P (a + c) (b + c)

source

@[simp]

theorem ite_mul {α : Type u_1} [has_mul α] (P : Prop) [decidable P] (a b c : α) :

ite P a b * c = ite P (a * c) (b * c)

source

@[simp]

theorem mul_boole {α : Type u_1} [mul_zero_one_class α] (P : Prop) [decidable P] (a : α) :

a * ite P 1 0 = ite P a 0

source

@[simp]

theorem boole_mul {α : Type u_1} [mul_zero_one_class α] (P : Prop) [decidable P] (a : α) :

ite P 1 0 * a = ite P a 0

source

theorem ite_mul_zero_left {α : Type u_1} [mul_zero_class α] (P : Prop) [decidable P] (a b : α) :

ite P (a * b) 0 = ite P a 0 * b

source

theorem ite_mul_zero_right {α : Type u_1} [mul_zero_class α] (P : Prop) [decidable P] (a b : α) :

ite P (a * b) 0 = a * ite P b 0

source

theorem ite_and_mul_zero {α : Type u_1} [mul_zero_class α] (P Q : Prop) [decidable P] [decidable Q] (a b : α) :

ite (P ∧ Q) (a * b) 0 = ite P a 0 * ite Q b 0

source

@[class]

structure non_unital_comm_semiring (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), non_unital_comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), non_unital_comm_semiring.nsmul n.succ x = x + non_unital_comm_semiring.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
mul_comm : ∀ (a b : α), a * b = b * a

A non-unital commutative semiring is a non_unital_semiring with commutative multiplication. In other words, it is a type with the following structures: additive commutative monoid (add_comm_monoid), commutative semigroup (comm_semigroup), distributive laws (distrib), and multiplication by zero law (mul_zero_class).

Instances of this typeclass

Instances of other typeclasses for non_unital_comm_semiring

non_unital_comm_semiring.has_sizeof_inst

source

@[instance]

def non_unital_comm_semiring.to_comm_semigroup (α : Type u) [self : non_unital_comm_semiring α] :

comm_semigroup α

source

@[instance]

def non_unital_comm_semiring.to_non_unital_semiring (α : Type u) [self : non_unital_comm_semiring α] :

non_unital_semiring α

source

@[class]

structure comm_semiring (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), comm_semiring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), comm_semiring.nsmul n.succ x = x + comm_semiring.nsmul n x) . "try_refl_tac"
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
nat_cast : ℕ → α
nat_cast_zero : comm_semiring.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), comm_semiring.nat_cast (n + 1) = comm_semiring.nat_cast n + 1) . "control_laws_tac"
npow : ℕ → α → α
npow_zero' : (∀ (x : α), comm_semiring.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), comm_semiring.npow n.succ x = x * comm_semiring.npow n x) . "try_refl_tac"
mul_comm : ∀ (a b : α), a * b = b * a

A commutative semiring is a semiring with commutative multiplication. In other words, it is a type with the following structures: additive commutative monoid (add_comm_monoid), multiplicative commutative monoid (comm_monoid), distributive laws (distrib), and multiplication by zero law (mul_zero_class).

Instances of this typeclass

Instances of other typeclasses for comm_semiring

comm_semiring.has_sizeof_inst

source

@[instance]

def comm_semiring.to_comm_monoid (α : Type u) [self : comm_semiring α] :

comm_monoid α

source

@[instance]

def comm_semiring.to_semiring (α : Type u) [self : comm_semiring α] :

semiring α

source

@[protected, instance]

def comm_semiring.to_non_unital_comm_semiring {α : Type u} [comm_semiring α] :

non_unital_comm_semiring α

Equations

comm_semiring.to_non_unital_comm_semiring = {add := semiring.add (comm_semiring.to_semiring α), add_assoc := _, zero := semiring.zero (comm_semiring.to_semiring α), zero_add := _, add_zero := _, nsmul := semiring.nsmul (comm_semiring.to_semiring α), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_monoid.mul (comm_semiring.to_comm_monoid α), left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}

source

@[protected, instance]

def comm_semiring.to_comm_monoid_with_zero {α : Type u} [comm_semiring α] :

comm_monoid_with_zero α

Equations

comm_semiring.to_comm_monoid_with_zero = {mul := comm_monoid.mul (comm_semiring.to_comm_monoid α), mul_assoc := _, one := comm_monoid.one (comm_semiring.to_comm_monoid α), one_mul := _, mul_one := _, npow := comm_monoid.npow (comm_semiring.to_comm_monoid α), npow_zero' := _, npow_succ' := _, mul_comm := _, zero := semiring.zero (comm_semiring.to_semiring α), zero_mul := _, mul_zero := _}

source

theorem add_mul_self_eq {α : Type u} [comm_semiring α] (a b : α) :

(a + b) * (a + b) = a * a + 2 * a * b + b * b

source

@[instance]

def has_distrib_neg.to_has_involutive_neg (α : Type u_1) [has_mul α] [self : has_distrib_neg α] :

has_involutive_neg α

source

@[class]

structure has_distrib_neg (α : Type u_1) [has_mul α] :

Type u_1

neg : α → α
neg_neg : ∀ (x : α), --x = x
neg_mul : ∀ (x y : α), -x * y = -(x * y)
mul_neg : ∀ (x y : α), x * -y = -(x * y)

Typeclass for a negation operator that distributes across multiplication.

This is useful for dealing with submonoids of a ring that contain -1 without having to duplicate lemmas.

Instances of this typeclass

Instances of other typeclasses for has_distrib_neg

has_distrib_neg.has_sizeof_inst

source

@[simp]

theorem neg_mul {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :

-a * b = -(a * b)

source

@[simp]

theorem mul_neg {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :

a * -b = -(a * b)

source

theorem neg_mul_neg {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :

-a * -b = a * b

source

theorem neg_mul_eq_neg_mul {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :

-(a * b) = -a * b

source

theorem neg_mul_eq_mul_neg {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :

-(a * b) = a * -b

source

theorem neg_mul_comm {α : Type u} [has_mul α] [has_distrib_neg α] (a b : α) :

-a * b = a * -b

source

theorem neg_eq_neg_one_mul {α : Type u} [mul_one_class α] [has_distrib_neg α] (a : α) :

-a = (-1) * a

source

theorem mul_neg_one {α : Type u} [mul_one_class α] [has_distrib_neg α] (a : α) :

a * -1 = -a

An element of a ring multiplied by the additive inverse of one is the element's additive inverse.

source

theorem neg_one_mul {α : Type u} [mul_one_class α] [has_distrib_neg α] (a : α) :

(-1) * a = -a

The additive inverse of one multiplied by an element of a ring is the element's additive inverse.

source

@[protected, instance]

def mul_zero_class.neg_zero_class {α : Type u} [mul_zero_class α] [has_distrib_neg α] :

neg_zero_class α

Equations

mul_zero_class.neg_zero_class = {zero := 0, neg := has_involutive_neg.neg (has_distrib_neg.to_has_involutive_neg α), neg_zero := _}

source

@[instance]

def non_unital_non_assoc_ring.to_non_unital_non_assoc_semiring (α : Type u) [self : non_unital_non_assoc_ring α] :

non_unital_non_assoc_semiring α

source

@[class]

structure non_unital_non_assoc_ring (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), non_unital_non_assoc_ring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), non_unital_non_assoc_ring.nsmul n.succ x = x + non_unital_non_assoc_ring.nsmul n x) . "try_refl_tac"
neg : α → α
sub : α → α → α
sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
zsmul : ℤ → α → α
zsmul_zero' : (∀ (a : α), non_unital_non_assoc_ring.zsmul 0 a = 0) . "try_refl_tac"
zsmul_succ' : (∀ (n : ℕ) (a : α), non_unital_non_assoc_ring.zsmul (int.of_nat n.succ) a = a + non_unital_non_assoc_ring.zsmul (int.of_nat n) a) . "try_refl_tac"
zsmul_neg' : (∀ (n : ℕ) (a : α), non_unital_non_assoc_ring.zsmul -[1+ n] a = -non_unital_non_assoc_ring.zsmul ↑(n.succ) a) . "try_refl_tac"
add_left_neg : ∀ (a : α), -a + a = 0
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0

A not-necessarily-unital, not-necessarily-associative ring.

Instances of this typeclass

Instances of other typeclasses for non_unital_non_assoc_ring

non_unital_non_assoc_ring.has_sizeof_inst

source

@[instance]

def non_unital_non_assoc_ring.to_add_comm_group (α : Type u) [self : non_unital_non_assoc_ring α] :

add_comm_group α

source

@[instance]

def non_unital_ring.to_non_unital_semiring (α : Type u_1) [self : non_unital_ring α] :

non_unital_semiring α

source

@[class]

structure non_unital_ring (α : Type u_1) :

Type u_1

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), non_unital_ring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), non_unital_ring.nsmul n.succ x = x + non_unital_ring.nsmul n x) . "try_refl_tac"
neg : α → α
sub : α → α → α
sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
zsmul : ℤ → α → α
zsmul_zero' : (∀ (a : α), non_unital_ring.zsmul 0 a = 0) . "try_refl_tac"
zsmul_succ' : (∀ (n : ℕ) (a : α), non_unital_ring.zsmul (int.of_nat n.succ) a = a + non_unital_ring.zsmul (int.of_nat n) a) . "try_refl_tac"
zsmul_neg' : (∀ (n : ℕ) (a : α), non_unital_ring.zsmul -[1+ n] a = -non_unital_ring.zsmul ↑(n.succ) a) . "try_refl_tac"
add_left_neg : ∀ (a : α), -a + a = 0
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)

An associative but not-necessarily unital ring.

Instances of this typeclass

Instances of other typeclasses for non_unital_ring

non_unital_ring.has_sizeof_inst

source

@[instance]

def non_unital_ring.to_non_unital_non_assoc_ring (α : Type u_1) [self : non_unital_ring α] :

non_unital_non_assoc_ring α

source

@[class]

structure non_assoc_ring (α : Type u_1) :

Type u_1

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), non_assoc_ring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), non_assoc_ring.nsmul n.succ x = x + non_assoc_ring.nsmul n x) . "try_refl_tac"
neg : α → α
sub : α → α → α
sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
zsmul : ℤ → α → α
zsmul_zero' : (∀ (a : α), non_assoc_ring.zsmul 0 a = 0) . "try_refl_tac"
zsmul_succ' : (∀ (n : ℕ) (a : α), non_assoc_ring.zsmul (int.of_nat n.succ) a = a + non_assoc_ring.zsmul (int.of_nat n) a) . "try_refl_tac"
zsmul_neg' : (∀ (n : ℕ) (a : α), non_assoc_ring.zsmul -[1+ n] a = -non_assoc_ring.zsmul ↑(n.succ) a) . "try_refl_tac"
add_left_neg : ∀ (a : α), -a + a = 0
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
one : α
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
nat_cast : ℕ → α
nat_cast_zero : non_assoc_ring.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), non_assoc_ring.nat_cast (n + 1) = non_assoc_ring.nat_cast n + 1) . "control_laws_tac"
int_cast : ℤ → α
int_cast_of_nat : (∀ (n : ℕ), non_assoc_ring.int_cast ↑n = ↑n) . "control_laws_tac"
int_cast_neg_succ_of_nat : (∀ (n : ℕ), non_assoc_ring.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"

A unital but not-necessarily-associative ring.

Instances of this typeclass

Instances of other typeclasses for non_assoc_ring

non_assoc_ring.has_sizeof_inst

source

@[instance]

def non_assoc_ring.to_add_comm_group_with_one (α : Type u_1) [self : non_assoc_ring α] :

add_comm_group_with_one α

source

@[instance]

def non_assoc_ring.to_non_assoc_semiring (α : Type u_1) [self : non_assoc_ring α] :

non_assoc_semiring α

source

@[instance]

def non_assoc_ring.to_non_unital_non_assoc_ring (α : Type u_1) [self : non_assoc_ring α] :

non_unital_non_assoc_ring α

source

@[instance]

def ring.to_monoid (α : Type u) [self : ring α] :

monoid α

source

@[instance]

def ring.to_add_comm_group_with_one (α : Type u) [self : ring α] :

add_comm_group_with_one α

source

@[class]

structure ring (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), ring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), ring.nsmul n.succ x = x + ring.nsmul n x) . "try_refl_tac"
neg : α → α
sub : α → α → α
sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
zsmul : ℤ → α → α
zsmul_zero' : (∀ (a : α), ring.zsmul 0 a = 0) . "try_refl_tac"
zsmul_succ' : (∀ (n : ℕ) (a : α), ring.zsmul (int.of_nat n.succ) a = a + ring.zsmul (int.of_nat n) a) . "try_refl_tac"
zsmul_neg' : (∀ (n : ℕ) (a : α), ring.zsmul -[1+ n] a = -ring.zsmul ↑(n.succ) a) . "try_refl_tac"
add_left_neg : ∀ (a : α), -a + a = 0
add_comm : ∀ (a b : α), a + b = b + a
int_cast : ℤ → α
nat_cast : ℕ → α
one : α
nat_cast_zero : ring.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), ring.nat_cast (n + 1) = ring.nat_cast n + 1) . "control_laws_tac"
int_cast_of_nat : (∀ (n : ℕ), ring.int_cast ↑n = ↑n) . "control_laws_tac"
int_cast_neg_succ_of_nat : (∀ (n : ℕ), ring.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
mul : α → α → α
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
npow : ℕ → α → α
npow_zero' : (∀ (x : α), ring.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), ring.npow n.succ x = x * ring.npow n x) . "try_refl_tac"
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c

A ring is a type with the following structures: additive commutative group (add_comm_group), multiplicative monoid (monoid), and distributive laws (distrib). Equivalently, a ring is a semiring with a negation operation making it an additive group.

Instances of this typeclass

Instances of other typeclasses for ring

ring.has_sizeof_inst

source

@[instance]

def ring.to_distrib (α : Type u) [self : ring α] :

distrib α

source

@[protected, instance]

def non_unital_non_assoc_ring.to_has_distrib_neg {α : Type u} [non_unital_non_assoc_ring α] :

has_distrib_neg α

Equations

non_unital_non_assoc_ring.to_has_distrib_neg = {neg := has_neg.neg (sub_neg_monoid.to_has_neg α), neg_neg := _, neg_mul := _, mul_neg := _}

source

theorem mul_sub_left_distrib {α : Type u} [non_unital_non_assoc_ring α] (a b c : α) :

a * (b - c) = a * b - a * c

source

theorem mul_sub {α : Type u} [non_unital_non_assoc_ring α] (a b c : α) :

a * (b - c) = a * b - a * c

Alias of mul_sub_left_distrib.

source

theorem mul_sub_right_distrib {α : Type u} [non_unital_non_assoc_ring α] (a b c : α) :

(a - b) * c = a * c - b * c

source

theorem sub_mul {α : Type u} [non_unital_non_assoc_ring α] (a b c : α) :

(a - b) * c = a * c - b * c

Alias of mul_sub_right_distrib.

source

theorem mul_add_eq_mul_add_iff_sub_mul_add_eq {α : Type u} [non_unital_non_assoc_ring α] {a b c d e : α} :

a * e + c = b * e + d ↔ (a - b) * e + c = d

An iff statement following from right distributivity in rings and the definition of subtraction.

source

theorem sub_mul_add_eq_of_mul_add_eq_mul_add {α : Type u} [non_unital_non_assoc_ring α] {a b c d e : α} :

a * e + c = b * e + d → (a - b) * e + c = d

A simplification of one side of an equation exploiting right distributivity in rings and the definition of subtraction.

source

theorem sub_one_mul {α : Type u} [non_assoc_ring α] (a b : α) :

(a - 1) * b = a * b - b

source

theorem mul_sub_one {α : Type u} [non_assoc_ring α] (a b : α) :

a * (b - 1) = a * b - a

source

theorem one_sub_mul {α : Type u} [non_assoc_ring α] (a b : α) :

(1 - a) * b = b - a * b

source

theorem mul_one_sub {α : Type u} [non_assoc_ring α] (a b : α) :

a * (1 - b) = a - a * b

source

@[protected, instance]

def ring.to_non_unital_ring {α : Type u} [ring α] :

non_unital_ring α

Equations

ring.to_non_unital_ring = {add := ring.add _inst_1, add_assoc := _, zero := ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg _inst_1, sub := ring.sub _inst_1, sub_eq_add_neg := _, zsmul := ring.zsmul _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _}

source

@[protected, instance]

def ring.to_non_assoc_ring {α : Type u} [ring α] :

non_assoc_ring α

Equations

ring.to_non_assoc_ring = {add := ring.add _inst_1, add_assoc := _, zero := ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg _inst_1, sub := ring.sub _inst_1, sub_eq_add_neg := _, zsmul := ring.zsmul _inst_1, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, one := ring.one _inst_1, one_mul := _, mul_one := _, nat_cast := ring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, int_cast := ring.int_cast _inst_1, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}

source

@[protected, instance]

def ring.to_semiring {α : Type u} [ring α] :

semiring α

Equations

ring.to_semiring = {add := ring.add _inst_1, add_assoc := _, zero := ring.zero _inst_1, zero_add := _, add_zero := _, nsmul := ring.nsmul _inst_1, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := ring.mul _inst_1, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := ring.one _inst_1, one_mul := _, mul_one := _, nat_cast := ring.nat_cast _inst_1, nat_cast_zero := _, nat_cast_succ := _, npow := ring.npow _inst_1, npow_zero' := _, npow_succ' := _}

source

@[class]

structure non_unital_comm_ring (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), non_unital_comm_ring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), non_unital_comm_ring.nsmul n.succ x = x + non_unital_comm_ring.nsmul n x) . "try_refl_tac"
neg : α → α
sub : α → α → α
sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
zsmul : ℤ → α → α
zsmul_zero' : (∀ (a : α), non_unital_comm_ring.zsmul 0 a = 0) . "try_refl_tac"
zsmul_succ' : (∀ (n : ℕ) (a : α), non_unital_comm_ring.zsmul (int.of_nat n.succ) a = a + non_unital_comm_ring.zsmul (int.of_nat n) a) . "try_refl_tac"
zsmul_neg' : (∀ (n : ℕ) (a : α), non_unital_comm_ring.zsmul -[1+ n] a = -non_unital_comm_ring.zsmul ↑(n.succ) a) . "try_refl_tac"
add_left_neg : ∀ (a : α), -a + a = 0
add_comm : ∀ (a b : α), a + b = b + a
mul : α → α → α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
zero_mul : ∀ (a : α), 0 * a = 0
mul_zero : ∀ (a : α), a * 0 = 0
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
mul_comm : ∀ (a b : α), a * b = b * a

A non-unital commutative ring is a non_unital_ring with commutative multiplication.

Instances of this typeclass

Instances of other typeclasses for non_unital_comm_ring

non_unital_comm_ring.has_sizeof_inst

source

@[instance]

def non_unital_comm_ring.to_comm_semigroup (α : Type u) [self : non_unital_comm_ring α] :

comm_semigroup α

source

@[instance]

def non_unital_comm_ring.to_non_unital_ring (α : Type u) [self : non_unital_comm_ring α] :

non_unital_ring α

source

@[protected, instance]

def non_unital_comm_ring.to_non_unital_comm_semiring {α : Type u} [s : non_unital_comm_ring α] :

non_unital_comm_semiring α

Equations

non_unital_comm_ring.to_non_unital_comm_semiring = {add := non_unital_comm_ring.add s, add_assoc := _, zero := non_unital_comm_ring.zero s, zero_add := _, add_zero := _, nsmul := non_unital_comm_ring.nsmul s, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := non_unital_comm_ring.mul s, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}

source

@[instance]

def comm_ring.to_ring (α : Type u) [self : comm_ring α] :

ring α

source

@[class]

structure comm_ring (α : Type u) :

Type u

add : α → α → α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
zero : α
zero_add : ∀ (a : α), 0 + a = a
add_zero : ∀ (a : α), a + 0 = a
nsmul : ℕ → α → α
nsmul_zero' : (∀ (x : α), comm_ring.nsmul 0 x = 0) . "try_refl_tac"
nsmul_succ' : (∀ (n : ℕ) (x : α), comm_ring.nsmul n.succ x = x + comm_ring.nsmul n x) . "try_refl_tac"
neg : α → α
sub : α → α → α
sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
zsmul : ℤ → α → α
zsmul_zero' : (∀ (a : α), comm_ring.zsmul 0 a = 0) . "try_refl_tac"
zsmul_succ' : (∀ (n : ℕ) (a : α), comm_ring.zsmul (int.of_nat n.succ) a = a + comm_ring.zsmul (int.of_nat n) a) . "try_refl_tac"
zsmul_neg' : (∀ (n : ℕ) (a : α), comm_ring.zsmul -[1+ n] a = -comm_ring.zsmul ↑(n.succ) a) . "try_refl_tac"
add_left_neg : ∀ (a : α), -a + a = 0
add_comm : ∀ (a b : α), a + b = b + a
int_cast : ℤ → α
nat_cast : ℕ → α
one : α
nat_cast_zero : comm_ring.nat_cast 0 = 0 . "control_laws_tac"
nat_cast_succ : (∀ (n : ℕ), comm_ring.nat_cast (n + 1) = comm_ring.nat_cast n + 1) . "control_laws_tac"
int_cast_of_nat : (∀ (n : ℕ), comm_ring.int_cast ↑n = ↑n) . "control_laws_tac"
int_cast_neg_succ_of_nat : (∀ (n : ℕ), comm_ring.int_cast (-↑(n + 1)) = -↑(n + 1)) . "control_laws_tac"
mul : α → α → α
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
one_mul : ∀ (a : α), 1 * a = a
mul_one : ∀ (a : α), a * 1 = a
npow : ℕ → α → α
npow_zero' : (∀ (x : α), comm_ring.npow 0 x = 1) . "try_refl_tac"
npow_succ' : (∀ (n : ℕ) (x : α), comm_ring.npow n.succ x = x * comm_ring.npow n x) . "try_refl_tac"
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
mul_comm : ∀ (a b : α), a * b = b * a

A commutative ring is a ring with commutative multiplication.

Instances of this typeclass

Instances of other typeclasses for comm_ring

comm_ring.has_sizeof_inst

source

@[instance]

def comm_ring.to_comm_monoid (α : Type u) [self : comm_ring α] :

comm_monoid α

source

@[protected, instance]

def comm_ring.to_comm_semiring {α : Type u} [s : comm_ring α] :

comm_semiring α

Equations

comm_ring.to_comm_semiring = {add := comm_ring.add s, add_assoc := _, zero := comm_ring.zero s, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul s, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_ring.mul s, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_ring.one s, one_mul := _, mul_one := _, nat_cast := comm_ring.nat_cast s, nat_cast_zero := _, nat_cast_succ := _, npow := comm_ring.npow s, npow_zero' := _, npow_succ' := _, mul_comm := _}

source

@[protected, instance]

def comm_ring.to_non_unital_comm_ring {α : Type u} [s : comm_ring α] :

non_unital_comm_ring α

Equations

comm_ring.to_non_unital_comm_ring = {add := comm_ring.add s, add_assoc := _, zero := comm_ring.zero s, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul s, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg s, sub := comm_ring.sub s, sub_eq_add_neg := _, zsmul := comm_ring.zsmul s, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul s, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, mul_comm := _}

source

@[instance]

def is_domain.to_is_cancel_mul_zero (α : Type u) [semiring α] [self : is_domain α] :

is_cancel_mul_zero α

source

@[class]

structure is_domain (α : Type u) [semiring α] :

Prop

mul_left_cancel_of_ne_zero : ∀ {a b c : α}, a ≠ 0 → a * b = a * c → b = c
mul_right_cancel_of_ne_zero : ∀ {a b c : α}, b ≠ 0 → a * b = c * b → a = c
exists_pair_ne : ∃ (x y : α), x ≠ y

A domain is a nontrivial semiring such multiplication by a non zero element is cancellative, on both sides. In other words, a nontrivial semiring R satisfying ∀ {a b c : R}, a ≠ 0 → a * b = a * c → b = c and ∀ {a b c : R}, b ≠ 0 → a * b = c * b → a = c.

This is implemented as a mixin for semiring α. To obtain an integral domain use [comm_ring α] [is_domain α].

Instances of this typeclass

source

@[instance]

def is_domain.to_nontrivial (α : Type u) [semiring α] [self : is_domain α] :

nontrivial α

mathlib3 documentation

Semirings and rings #

Main definitions #

Tags #

`distrib` class #

Semirings #

Rings #

Semirings and rings #

Main definitions #

Tags #

distrib class #

Semirings #

Rings #

`distrib` class #