mathlib documentation

algebra.opposites

Algebraic operations on αᵒᵖ

@[instance]
def opposite.has_add (α : Type u) [has_add α] :

Equations
@[instance]
def opposite.has_zero (α : Type u) [has_zero α] :

Equations
@[instance]
def opposite.nontrivial (α : Type u) [nontrivial α] :

@[simp]
theorem opposite.unop_eq_zero_iff (α : Type u) [has_zero α] (a : αᵒᵖ) :

@[simp]
theorem opposite.op_eq_zero_iff (α : Type u) [has_zero α] (a : α) :
opposite.op a = 0 a = 0

@[instance]
def opposite.add_monoid (α : Type u) [add_monoid α] :

Equations
@[instance]
def opposite.has_neg (α : Type u) [has_neg α] :

Equations
@[instance]
def opposite.has_mul (α : Type u) [has_mul α] :

Equations
@[instance]
def opposite.semigroup (α : Type u) [semigroup α] :

Equations
@[instance]
def opposite.has_one (α : Type u) [has_one α] :

Equations
@[simp]
theorem opposite.unop_eq_one_iff (α : Type u) [has_one α] (a : αᵒᵖ) :

@[simp]
theorem opposite.op_eq_one_iff (α : Type u) [has_one α] (a : α) :
opposite.op a = 1 a = 1

@[instance]
def opposite.monoid (α : Type u) [monoid α] :

Equations
@[instance]
def opposite.comm_monoid (α : Type u) [comm_monoid α] :

Equations
@[instance]
def opposite.has_inv (α : Type u) [has_inv α] :

Equations
@[instance]
def opposite.group (α : Type u) [group α] :

Equations
@[instance]
def opposite.comm_group (α : Type u) [comm_group α] :

Equations
@[instance]
def opposite.distrib (α : Type u) [distrib α] :

Equations
@[instance]
def opposite.comm_ring (α : Type u) [comm_ring α] :

Equations
@[simp]
theorem opposite.op_zero (α : Type u) [has_zero α] :

@[simp]
theorem opposite.unop_zero (α : Type u) [has_zero α] :

@[simp]
theorem opposite.op_one (α : Type u) [has_one α] :

@[simp]
theorem opposite.unop_one (α : Type u) [has_one α] :

@[simp]
theorem opposite.op_add {α : Type u} [has_add α] (x y : α) :

@[simp]
theorem opposite.unop_add {α : Type u} [has_add α] (x y : αᵒᵖ) :

@[simp]
theorem opposite.op_neg {α : Type u} [has_neg α] (x : α) :

@[simp]
theorem opposite.unop_neg {α : Type u} [has_neg α] (x : αᵒᵖ) :

@[simp]
theorem opposite.op_mul {α : Type u} [has_mul α] (x y : α) :

@[simp]
theorem opposite.unop_mul {α : Type u} [has_mul α] (x y : αᵒᵖ) :

@[simp]
theorem opposite.op_inv {α : Type u} [has_inv α] (x : α) :

@[simp]
theorem opposite.unop_inv {α : Type u} [has_inv α] (x : αᵒᵖ) :

@[simp]
theorem opposite.op_sub {α : Type u} [add_group α] (x y : α) :

@[simp]
theorem opposite.unop_sub {α : Type u} [add_group α] (x y : αᵒᵖ) :

def opposite.op_add_hom {α : Type u} [add_comm_monoid α] :

The function op is a homomorphism of additive commutative monoids.

Equations
def opposite.unop_add_hom {α : Type u} [add_comm_monoid α] :

The function unop is a homomorphism of additive commutative monoids.

Equations