mathlib docs: algebra.opposites

source

@[instance]

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

has_add αᵒᵖ

Equations

opposite.has_add α = {add := λ (x y : αᵒᵖ), opposite.op (opposite.unop x + opposite.unop y)}

source

@[instance]

def opposite.add_semigroup (α : Type u) [add_semigroup α] :

add_semigroup αᵒᵖ

Equations

opposite.add_semigroup α = {add := has_add.add (opposite.has_add α), add_assoc := _}

source

@[instance]

def opposite.add_left_cancel_semigroup (α : Type u) [add_left_cancel_semigroup α] :

add_left_cancel_semigroup αᵒᵖ

Equations

opposite.add_left_cancel_semigroup α = {add := add_semigroup.add (opposite.add_semigroup α), add_assoc := _, add_left_cancel := _}

source

@[instance]

def opposite.add_right_cancel_semigroup (α : Type u) [add_right_cancel_semigroup α] :

add_right_cancel_semigroup αᵒᵖ

Equations

opposite.add_right_cancel_semigroup α = {add := add_semigroup.add (opposite.add_semigroup α), add_assoc := _, add_right_cancel := _}

source

@[instance]

def opposite.add_comm_semigroup (α : Type u) [add_comm_semigroup α] :

add_comm_semigroup αᵒᵖ

Equations

opposite.add_comm_semigroup α = {add := add_semigroup.add (opposite.add_semigroup α), add_assoc := _, add_comm := _}

source

@[instance]

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

has_zero αᵒᵖ

Equations

opposite.has_zero α = {zero := opposite.op 0}

source

@[instance]

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

nontrivial αᵒᵖ

source

@[simp]

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

opposite.unop a = 0 ↔ a = 0

source

@[simp]

theorem opposite.op_eq_zero_iff (α : Type u) [has_zero α] (a : α) :

opposite.op a = 0 ↔ a = 0

source

@[instance]

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

add_monoid αᵒᵖ

Equations

opposite.add_monoid α = {add := add_semigroup.add (opposite.add_semigroup α), add_assoc := _, zero := 0, zero_add := _, add_zero := _}

source

@[instance]

def opposite.add_comm_monoid (α : Type u) [add_comm_monoid α] :

add_comm_monoid αᵒᵖ

Equations

opposite.add_comm_monoid α = {add := add_monoid.add (opposite.add_monoid α), add_assoc := _, zero := add_monoid.zero (opposite.add_monoid α), zero_add := _, add_zero := _, add_comm := _}

source

@[instance]

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

has_neg αᵒᵖ

Equations

opposite.has_neg α = {neg := λ (x : αᵒᵖ), opposite.op (-opposite.unop x)}

source

@[instance]

def opposite.add_group (α : Type u) [add_group α] :

add_group αᵒᵖ

Equations

opposite.add_group α = {add := add_monoid.add (opposite.add_monoid α), add_assoc := _, zero := add_monoid.zero (opposite.add_monoid α), zero_add := _, add_zero := _, neg := has_neg.neg (opposite.has_neg α), add_left_neg := _}

source

@[instance]

def opposite.add_comm_group (α : Type u) [add_comm_group α] :

add_comm_group αᵒᵖ

Equations

opposite.add_comm_group α = {add := add_group.add (opposite.add_group α), add_assoc := _, zero := add_group.zero (opposite.add_group α), zero_add := _, add_zero := _, neg := add_group.neg (opposite.add_group α), add_left_neg := _, add_comm := _}

source

@[instance]

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

has_mul αᵒᵖ

Equations

opposite.has_mul α = {mul := λ (x y : αᵒᵖ), opposite.op ((opposite.unop y) * opposite.unop x)}

source

@[instance]

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

semigroup αᵒᵖ

Equations

opposite.semigroup α = {mul := has_mul.mul (opposite.has_mul α), mul_assoc := _}

source

@[instance]

def opposite.left_cancel_semigroup (α : Type u) [right_cancel_semigroup α] :

left_cancel_semigroup αᵒᵖ

Equations

opposite.left_cancel_semigroup α = {mul := semigroup.mul (opposite.semigroup α), mul_assoc := _, mul_left_cancel := _}

source

@[instance]

def opposite.right_cancel_semigroup (α : Type u) [left_cancel_semigroup α] :

right_cancel_semigroup αᵒᵖ

Equations

opposite.right_cancel_semigroup α = {mul := semigroup.mul (opposite.semigroup α), mul_assoc := _, mul_right_cancel := _}

source

@[instance]

def opposite.comm_semigroup (α : Type u) [comm_semigroup α] :

comm_semigroup αᵒᵖ

Equations

opposite.comm_semigroup α = {mul := semigroup.mul (opposite.semigroup α), mul_assoc := _, mul_comm := _}

source

@[instance]

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

has_one αᵒᵖ

Equations

opposite.has_one α = {one := opposite.op 1}

source

@[simp]

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

opposite.unop a = 1 ↔ a = 1

source

@[simp]

theorem opposite.op_eq_one_iff (α : Type u) [has_one α] (a : α) :

opposite.op a = 1 ↔ a = 1

source

@[instance]

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

monoid αᵒᵖ

Equations

opposite.monoid α = {mul := semigroup.mul (opposite.semigroup α), mul_assoc := _, one := 1, one_mul := _, mul_one := _}

source

@[instance]

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

comm_monoid αᵒᵖ

Equations

opposite.comm_monoid α = {mul := monoid.mul (opposite.monoid α), mul_assoc := _, one := monoid.one (opposite.monoid α), one_mul := _, mul_one := _, mul_comm := _}

source

@[instance]

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

has_inv αᵒᵖ

Equations

opposite.has_inv α = {inv := λ (x : αᵒᵖ), opposite.op (opposite.unop x)⁻¹}

source

@[instance]

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

group αᵒᵖ

Equations

opposite.group α = {mul := monoid.mul (opposite.monoid α), mul_assoc := _, one := monoid.one (opposite.monoid α), one_mul := _, mul_one := _, inv := has_inv.inv (opposite.has_inv α), mul_left_inv := _}

source

@[instance]

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

comm_group αᵒᵖ

Equations

opposite.comm_group α = {mul := group.mul (opposite.group α), mul_assoc := _, one := group.one (opposite.group α), one_mul := _, mul_one := _, inv := group.inv (opposite.group α), mul_left_inv := _, mul_comm := _}

source

@[instance]

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

distrib αᵒᵖ

Equations

opposite.distrib α = {mul := has_mul.mul (opposite.has_mul α), add := has_add.add (opposite.has_add α), left_distrib := _, right_distrib := _}

source

@[instance]

def opposite.semiring (α : Type u) [semiring α] :

semiring αᵒᵖ

Equations

opposite.semiring α = {add := add_comm_monoid.add (opposite.add_comm_monoid α), add_assoc := _, zero := add_comm_monoid.zero (opposite.add_comm_monoid α), zero_add := _, add_zero := _, add_comm := _, mul := monoid.mul (opposite.monoid α), mul_assoc := _, one := monoid.one (opposite.monoid α), one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}

source

@[instance]

def opposite.ring (α : Type u) [ring α] :

ring αᵒᵖ

Equations

opposite.ring α = {add := add_comm_group.add (opposite.add_comm_group α), add_assoc := _, zero := add_comm_group.zero (opposite.add_comm_group α), zero_add := _, add_zero := _, neg := add_comm_group.neg (opposite.add_comm_group α), add_left_neg := _, add_comm := _, mul := monoid.mul (opposite.monoid α), mul_assoc := _, one := monoid.one (opposite.monoid α), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}

source

@[instance]

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

comm_ring αᵒᵖ

Equations

opposite.comm_ring α = {add := ring.add (opposite.ring α), add_assoc := _, zero := ring.zero (opposite.ring α), zero_add := _, add_zero := _, neg := ring.neg (opposite.ring α), add_left_neg := _, add_comm := _, mul := ring.mul (opposite.ring α), mul_assoc := _, one := ring.one (opposite.ring α), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

@[instance]

def opposite.integral_domain (α : Type u) [integral_domain α] :

integral_domain αᵒᵖ

Equations

opposite.integral_domain α = {add := comm_ring.add (opposite.comm_ring α), add_assoc := _, zero := comm_ring.zero (opposite.comm_ring α), zero_add := _, add_zero := _, neg := comm_ring.neg (opposite.comm_ring α), add_left_neg := _, add_comm := _, mul := comm_ring.mul (opposite.comm_ring α), mul_assoc := _, one := comm_ring.one (opposite.comm_ring α), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}

source

@[instance]

def opposite.field (α : Type u) [field α] :

field αᵒᵖ

Equations

opposite.field α = {add := comm_ring.add (opposite.comm_ring α), add_assoc := _, zero := comm_ring.zero (opposite.comm_ring α), zero_add := _, add_zero := _, neg := comm_ring.neg (opposite.comm_ring α), add_left_neg := _, add_comm := _, mul := comm_ring.mul (opposite.comm_ring α), mul_assoc := _, one := comm_ring.one (opposite.comm_ring α), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := has_inv.inv (opposite.has_inv α), exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}

source

@[simp]

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

opposite.op 0 = 0

source

@[simp]

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

opposite.unop 0 = 0

source

@[simp]

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

opposite.op 1 = 1

source

@[simp]

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

opposite.unop 1 = 1

source

@[simp]

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

opposite.op (x + y) = opposite.op x + opposite.op y

source

@[simp]

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

opposite.unop (x + y) = opposite.unop x + opposite.unop y

source

@[simp]

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

opposite.op (-x) = -opposite.op x

source

@[simp]

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

opposite.unop (-x) = -opposite.unop x

source

@[simp]

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

opposite.op (x * y) = (opposite.op y) * opposite.op x

source

@[simp]

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

opposite.unop (x * y) = (opposite.unop y) * opposite.unop x

source

@[simp]

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

opposite.op x⁻¹ = (opposite.op x)⁻¹

source

@[simp]

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

opposite.unop x⁻¹ = (opposite.unop x)⁻¹

source

@[simp]

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

opposite.op (x - y) = opposite.op x - opposite.op y

source

@[simp]

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

opposite.unop (x - y) = opposite.unop x - opposite.unop y

source

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

α →+ αᵒᵖ

The function op is a homomorphism of additive commutative monoids.

Equations

opposite.op_add_hom = {to_fun := opposite.op α, map_zero' := _, map_add' := _}

source

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

αᵒᵖ →+ α

The function unop is a homomorphism of additive commutative monoids.

Equations

opposite.unop_add_hom = {to_fun := opposite.unop α, map_zero' := _, map_add' := _}

source

@[simp]

theorem opposite.coe_op_add_hom {α : Type u} [add_comm_monoid α] :

⇑opposite.op_add_hom = opposite.op

source

@[simp]

theorem opposite.coe_unop_add_hom {α : Type u} [add_comm_monoid α] :

⇑opposite.unop_add_hom = opposite.unop