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.has_sub (α : Type u) [has_sub α] :

has_sub αᵒᵖ

Equations

opposite.has_sub α = {sub := λ (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 α), sub := has_sub.sub (opposite.has_sub α), sub_eq_add_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 α), sub := add_group.sub (opposite.add_group α), sub_eq_add_neg := _, 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 α), div := div_inv_monoid.div._default monoid.mul _ monoid.one _ _ has_inv.inv, div_eq_mul_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 α), div := group.div (opposite.group α), div_eq_mul_inv := _, 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 α), sub := add_comm_group.sub (opposite.add_comm_group α), sub_eq_add_neg := _, 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 α), sub := ring.sub (opposite.ring α), sub_eq_add_neg := _, 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 α), sub := comm_ring.sub (opposite.comm_ring α), sub_eq_add_neg := _, 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 α), sub := comm_ring.sub (opposite.comm_ring α), sub_eq_add_neg := _, 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

@[instance]

def opposite.has_scalar (α : Type u) (R : Type u_1) [has_scalar R α] :

has_scalar R αᵒᵖ

Equations

opposite.has_scalar α R = {smul := λ (c : R) (x : αᵒᵖ), opposite.op (c • opposite.unop x)}

source

@[instance]

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

mul_action R αᵒᵖ

Equations

opposite.mul_action α R = {to_has_scalar := {smul := has_scalar.smul (opposite.has_scalar α R)}, one_smul := _, mul_smul := _}

source

@[instance]

def opposite.distrib_mul_action (α : Type u) (R : Type u_1) [monoid R] [add_monoid α] [distrib_mul_action R α] :

distrib_mul_action R αᵒᵖ

Equations

opposite.distrib_mul_action α R = {to_mul_action := {to_has_scalar := mul_action.to_has_scalar (opposite.mul_action α R), one_smul := _, mul_smul := _}, smul_add := _, smul_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

@[simp]

theorem opposite.op_smul {α : Type u} {R : Type u_1} [has_scalar R α] (c : R) (a : α) :

opposite.op (c • a) = c • opposite.op a

source

@[simp]

theorem opposite.unop_smul {α : Type u} {R : Type u_1} [has_scalar R α] (c : R) (a : αᵒᵖ) :

opposite.unop (c • a) = c • opposite.unop a

source

def opposite.op_add_equiv {α : Type u} [has_add α] :

α ≃+ αᵒᵖ

The function op is an additive equivalence.

Equations

opposite.op_add_equiv = {to_fun := opposite.equiv_to_opposite.to_fun, inv_fun := opposite.equiv_to_opposite.inv_fun, left_inv := _, right_inv := _, map_add' := _}

source

@[simp]

theorem opposite.coe_op_add_equiv {α : Type u} [has_add α] :

⇑opposite.op_add_equiv = opposite.op

source

@[simp]

theorem opposite.coe_op_add_equiv_symm {α : Type u} [has_add α] :

⇑(opposite.op_add_equiv.symm) = opposite.unop

source

@[simp]

theorem opposite.op_add_equiv_to_equiv {α : Type u} [has_add α] :

opposite.op_add_equiv.to_equiv = opposite.equiv_to_opposite

source

def ring_hom.to_opposite {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R →+* S) (hf : ∀ (x y : R), commute (⇑f x) (⇑f y)) :

R →+* Sᵒᵖ

A ring homomorphism f : R →+* S such that f x commutes with f y for all x, y defines a ring homomorphism to Sᵒᵖ.

Equations

f.to_opposite hf = {to_fun := (opposite.op_add_equiv.to_add_monoid_hom.comp ↑f).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

@[simp]

theorem ring_hom.coe_to_opposite {R : Type u_1} {S : Type u_2} [semiring R] [semiring S] (f : R →+* S) (hf : ∀ (x y : R), commute (⇑f x) (⇑f y)) :

⇑(f.to_opposite hf) = opposite.op ∘ ⇑f

mathlib documentation

Algebraic operations on `αᵒᵖ`

Algebraic operations on αᵒᵖ

Algebraic operations on `αᵒᵖ`