# mathlib3documentation

algebra.opposites

# Multiplicative opposite and algebraic operations on it #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define mul_opposite α = αᵐᵒᵖ to be the multiplicative opposite of α. It inherits all additive algebraic structures on α (in other files), and reverses the order of multipliers in multiplicative structures, i.e., op (x * y) = op y * op x, where mul_opposite.op is the canonical map from α to αᵐᵒᵖ.

We also define add_opposite α = αᵃᵒᵖ to be the additive opposite of α. It inherits all multiplicative algebraic structures on α (in other files), and reverses the order of summands in additive structures, i.e. op (x + y) = op y + op x, where add_opposite.op is the canonical map from α to αᵃᵒᵖ.

## Notation #

• αᵐᵒᵖ = mul_opposite α
• αᵃᵒᵖ = add_opposite α

## Tags #

@[irreducible]
def mul_opposite (α : Type u) :

Multiplicative opposite of a type. This type inherits all additive structures on α and reverses left and right in multiplication.

Equations
Instances for mul_opposite
def add_opposite (α : Type u) :

Additive opposite of a type. This type inherits all multiplicative structures on α and reverses left and right in addition.

Equations
Instances for add_opposite
def mul_opposite.op {α : Type u} :

The element of mul_opposite α that represents x : α.

Equations
def add_opposite.op {α : Type u} :

The element of αᵃᵒᵖ that represents x : α.

Equations
def mul_opposite.unop {α : Type u} :

The element of α represented by x : αᵐᵒᵖ.

Equations
def add_opposite.unop {α : Type u} :

The element of α represented by x : αᵃᵒᵖ.

Equations
@[simp]
theorem mul_opposite.unop_op {α : Type u} (x : α) :
@[simp]
theorem add_opposite.unop_op {α : Type u} (x : α) :
@[simp]
theorem mul_opposite.op_unop {α : Type u} (x : αᵐᵒᵖ) :
@[simp]
theorem add_opposite.op_unop {α : Type u} (x : αᵃᵒᵖ) :
@[simp]
theorem add_opposite.op_comp_unop {α : Type u} :
@[simp]
theorem mul_opposite.op_comp_unop {α : Type u} :
@[simp]
theorem mul_opposite.unop_comp_op {α : Type u} :
@[simp]
theorem add_opposite.unop_comp_op {α : Type u} :
@[protected, simp]
def mul_opposite.rec {α : Type u} {F : αᵐᵒᵖ Sort v} (h : Π (X : α), F ) (X : αᵐᵒᵖ) :
F X

A recursor for mul_opposite. Use as induction x using mul_opposite.rec.

Equations
@[protected, simp]
def add_opposite.rec {α : Type u} {F : αᵃᵒᵖ Sort v} (h : Π (X : α), F ) (X : αᵃᵒᵖ) :
F X

A recursor for add_opposite. Use as induction x using add_opposite.rec.

Equations
@[simp]
theorem mul_opposite.op_equiv_apply {α : Type u} :
def mul_opposite.op_equiv {α : Type u} :

The canonical bijection between α and αᵐᵒᵖ.

Equations
@[simp]
theorem add_opposite.op_equiv_apply {α : Type u} :
@[simp]
@[simp]
def add_opposite.op_equiv {α : Type u} :

The canonical bijection between α and αᵃᵒᵖ.

Equations
theorem mul_opposite.op_bijective {α : Type u} :
theorem add_opposite.op_bijective {α : Type u} :
theorem mul_opposite.op_injective {α : Type u} :
theorem add_opposite.op_injective {α : Type u} :
theorem add_opposite.op_surjective {α : Type u} :
theorem mul_opposite.op_surjective {α : Type u} :
@[simp]
theorem add_opposite.op_inj {α : Type u} {x y : α} :
x = y
@[simp]
theorem mul_opposite.op_inj {α : Type u} {x y : α} :
x = y
@[simp]
theorem add_opposite.unop_inj {α : Type u} {x y : αᵃᵒᵖ} :
x = y
@[simp]
theorem mul_opposite.unop_inj {α : Type u} {x y : αᵐᵒᵖ} :
x = y
@[protected, instance]
def mul_opposite.nontrivial (α : Type u) [nontrivial α] :
@[protected, instance]
def add_opposite.nontrivial (α : Type u) [nontrivial α] :
@[protected, instance]
def add_opposite.inhabited (α : Type u) [inhabited α] :
Equations
@[protected, instance]
def mul_opposite.inhabited (α : Type u) [inhabited α] :
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def add_opposite.unique (α : Type u) [unique α] :
Equations
@[protected, instance]
def mul_opposite.unique (α : Type u) [unique α] :
Equations
@[protected, instance]
def mul_opposite.is_empty (α : Type u) [is_empty α] :
@[protected, instance]
def add_opposite.is_empty (α : Type u) [is_empty α] :
@[protected, instance]
def mul_opposite.has_zero (α : Type u) [has_zero α] :
Equations
@[protected, instance]
def mul_opposite.has_one (α : Type u) [has_one α] :
Equations
@[protected, instance]
def add_opposite.has_zero (α : Type u) [has_zero α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.has_sub (α : Type u) [has_sub α] :
Equations
@[protected, instance]
def mul_opposite.has_neg (α : Type u) [has_neg α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.has_mul (α : Type u) [has_mul α] :
Equations
@[protected, instance]
def mul_opposite.has_inv (α : Type u) [has_inv α] :
Equations
@[protected, instance]
def add_opposite.has_neg (α : Type u) [has_neg α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def add_opposite.has_vadd (α : Type u) (R : Type u_1) [ α] :
Equations
@[protected, instance]
def mul_opposite.has_smul (α : Type u) (R : Type u_1) [ α] :
Equations
@[simp]
theorem mul_opposite.op_zero (α : Type u) [has_zero α] :
@[simp]
theorem mul_opposite.unop_zero (α : Type u) [has_zero α] :
@[simp]
theorem add_opposite.op_zero (α : Type u) [has_zero α] :
@[simp]
theorem mul_opposite.op_one (α : Type u) [has_one α] :
@[simp]
theorem mul_opposite.unop_one (α : Type u) [has_one α] :
@[simp]
theorem add_opposite.unop_zero (α : Type u) [has_zero α] :
@[simp]
theorem mul_opposite.op_add {α : Type u} [has_add α] (x y : α) :
@[simp]
theorem mul_opposite.unop_add {α : Type u} [has_add α] (x y : αᵐᵒᵖ) :
@[simp]
theorem mul_opposite.op_neg {α : Type u} [has_neg α] (x : α) :
@[simp]
theorem mul_opposite.unop_neg {α : Type u} [has_neg α] (x : αᵐᵒᵖ) :
@[simp]
@[simp]
theorem mul_opposite.op_mul {α : Type u} [has_mul α] (x y : α) :
@[simp]
theorem mul_opposite.unop_mul {α : Type u} [has_mul α] (x y : αᵐᵒᵖ) :
@[simp]
@[simp]
theorem add_opposite.op_neg {α : Type u} [has_neg α] (x : α) :
@[simp]
theorem mul_opposite.op_inv {α : Type u} [has_inv α] (x : α) :
@[simp]
theorem mul_opposite.unop_inv {α : Type u} [has_inv α] (x : αᵐᵒᵖ) :
@[simp]
theorem add_opposite.unop_neg {α : Type u} [has_neg α] (x : αᵃᵒᵖ) :
@[simp]
theorem mul_opposite.op_sub {α : Type u} [has_sub α] (x y : α) :
@[simp]
theorem mul_opposite.unop_sub {α : Type u} [has_sub α] (x y : αᵐᵒᵖ) :
@[simp]
theorem add_opposite.op_vadd {α : Type u} {R : Type u_1} [ α] (c : R) (a : α) :
@[simp]
theorem mul_opposite.op_smul {α : Type u} {R : Type u_1} [ α] (c : R) (a : α) :
@[simp]
theorem mul_opposite.unop_smul {α : Type u} {R : Type u_1} [ α] (c : R) (a : αᵐᵒᵖ) :
@[simp]
theorem add_opposite.unop_vadd {α : Type u} {R : Type u_1} [ α] (c : R) (a : αᵃᵒᵖ) :
@[simp]
theorem mul_opposite.unop_eq_zero_iff {α : Type u} [has_zero α] (a : αᵐᵒᵖ) :
a = 0
@[simp]
theorem mul_opposite.op_eq_zero_iff {α : Type u} [has_zero α] (a : α) :
a = 0
theorem mul_opposite.unop_ne_zero_iff {α : Type u} [has_zero α] (a : αᵐᵒᵖ) :
a 0
theorem mul_opposite.op_ne_zero_iff {α : Type u} [has_zero α] (a : α) :
a 0
@[simp]
theorem mul_opposite.unop_eq_one_iff {α : Type u} [has_one α] (a : αᵐᵒᵖ) :
a = 1
@[simp]
theorem add_opposite.unop_eq_zero_iff {α : Type u} [has_zero α] (a : αᵃᵒᵖ) :
a = 0
@[simp]
theorem add_opposite.op_eq_zero_iff {α : Type u} [has_zero α] (a : α) :
a = 0
@[simp]
theorem mul_opposite.op_eq_one_iff {α : Type u} [has_one α] (a : α) :
a = 1
@[protected, instance]
def add_opposite.has_one {α : Type u} [has_one α] :
Equations
@[simp]
theorem add_opposite.op_one {α : Type u} [has_one α] :
@[simp]
theorem add_opposite.unop_one {α : Type u} [has_one α] :
@[simp]
theorem add_opposite.op_eq_one_iff {α : Type u} [has_one α] {a : α} :
a = 1
@[simp]
theorem add_opposite.unop_eq_one_iff {α : Type u} [has_one α] {a : αᵃᵒᵖ} :
a = 1
@[protected, instance]
def add_opposite.has_mul {α : Type u} [has_mul α] :
Equations
@[simp]
theorem add_opposite.op_mul {α : Type u} [has_mul α] (a b : α) :
@[simp]
theorem add_opposite.unop_mul {α : Type u} [has_mul α] (a b : αᵃᵒᵖ) :
@[protected, instance]
def add_opposite.has_inv {α : Type u} [has_inv α] :
Equations
@[protected, instance]
Equations
@[simp]
theorem add_opposite.op_inv {α : Type u} [has_inv α] (a : α) :
@[simp]
theorem add_opposite.unop_inv {α : Type u} [has_inv α] (a : αᵃᵒᵖ) :
@[protected, instance]
def add_opposite.has_div {α : Type u} [has_div α] :
Equations
@[simp]
theorem add_opposite.op_div {α : Type u} [has_div α] (a b : α) :
@[simp]
theorem add_opposite.unop_div {α : Type u} [has_div α] (a b : αᵃᵒᵖ) :