Algebraic operations on αᵒᵖ
@[instance]
Equations
- opposite.has_add α = {add := λ (x y : αᵒᵖ), opposite.op (opposite.unop x + opposite.unop y)}
@[instance]
Equations
- opposite.has_sub α = {sub := λ (x y : αᵒᵖ), opposite.op (opposite.unop x - opposite.unop y)}
@[instance]
Equations
- opposite.add_semigroup α = {add := has_add.add (opposite.has_add α), add_assoc := _}
@[instance]
Equations
- opposite.add_left_cancel_semigroup α = {add := add_semigroup.add (opposite.add_semigroup α), add_assoc := _, add_left_cancel := _}
@[instance]
Equations
- opposite.add_right_cancel_semigroup α = {add := add_semigroup.add (opposite.add_semigroup α), add_assoc := _, add_right_cancel := _}
@[instance]
Equations
- opposite.add_comm_semigroup α = {add := add_semigroup.add (opposite.add_semigroup α), add_assoc := _, add_comm := _}
@[instance]
Equations
- opposite.has_zero α = {zero := opposite.op 0}
@[simp]
@[simp]
@[instance]
Equations
- opposite.add_monoid α = {add := add_semigroup.add (opposite.add_semigroup α), add_assoc := _, zero := 0, zero_add := _, add_zero := _}
@[instance]
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 := _}
@[instance]
Equations
- opposite.has_neg α = {neg := λ (x : αᵒᵖ), opposite.op (-opposite.unop x)}
@[instance]
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 := _}
@[instance]
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 := _}
@[instance]
Equations
- opposite.has_mul α = {mul := λ (x y : αᵒᵖ), opposite.op ((opposite.unop y) * opposite.unop x)}
@[instance]
Equations
- opposite.semigroup α = {mul := has_mul.mul (opposite.has_mul α), mul_assoc := _}
@[instance]
Equations
- opposite.left_cancel_semigroup α = {mul := semigroup.mul (opposite.semigroup α), mul_assoc := _, mul_left_cancel := _}
@[instance]
Equations
- opposite.right_cancel_semigroup α = {mul := semigroup.mul (opposite.semigroup α), mul_assoc := _, mul_right_cancel := _}
@[instance]
Equations
- opposite.comm_semigroup α = {mul := semigroup.mul (opposite.semigroup α), mul_assoc := _, mul_comm := _}
@[instance]
Equations
- opposite.has_one α = {one := opposite.op 1}
@[simp]
@[simp]
@[instance]
Equations
- opposite.monoid α = {mul := semigroup.mul (opposite.semigroup α), mul_assoc := _, one := 1, one_mul := _, mul_one := _}
@[instance]
Equations
- opposite.comm_monoid α = {mul := monoid.mul (opposite.monoid α), mul_assoc := _, one := monoid.one (opposite.monoid α), one_mul := _, mul_one := _, mul_comm := _}
@[instance]
Equations
- opposite.has_inv α = {inv := λ (x : αᵒᵖ), opposite.op (opposite.unop x)⁻¹}
@[instance]
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 := _}
@[instance]
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 := _}
@[instance]
Equations
- opposite.distrib α = {mul := has_mul.mul (opposite.has_mul α), add := has_add.add (opposite.has_add α), left_distrib := _, right_distrib := _}
@[instance]
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 := _}
@[instance]
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 := _}
@[instance]
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 := _}
@[instance]
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 := _}
@[instance]
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 := _}
@[instance]
Equations
- opposite.has_scalar α R = {smul := λ (c : R) (x : αᵒᵖ), opposite.op (c • opposite.unop x)}
@[instance]
Equations
- opposite.mul_action α R = {to_has_scalar := {smul := has_scalar.smul (opposite.has_scalar α R)}, one_smul := _, mul_smul := _}
@[instance]
def
opposite.distrib_mul_action
(α : Type u)
(R : Type u_1)
[monoid R]
[add_monoid α]
[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 := _}
@[simp]
theorem
opposite.op_add
{α : Type u}
[has_add α]
(x y : α) :
opposite.op (x + y) = opposite.op x + opposite.op y
@[simp]
theorem
opposite.unop_add
{α : Type u}
[has_add α]
(x y : αᵒᵖ) :
opposite.unop (x + y) = opposite.unop x + opposite.unop y
@[simp]
@[simp]
theorem
opposite.unop_neg
{α : Type u}
[has_neg α]
(x : αᵒᵖ) :
opposite.unop (-x) = -opposite.unop x
@[simp]
theorem
opposite.op_mul
{α : Type u}
[has_mul α]
(x y : α) :
opposite.op (x * y) = (opposite.op y) * opposite.op x
@[simp]
theorem
opposite.unop_mul
{α : Type u}
[has_mul α]
(x y : αᵒᵖ) :
opposite.unop (x * y) = (opposite.unop y) * opposite.unop x
@[simp]
@[simp]
theorem
opposite.unop_inv
{α : Type u}
[has_inv α]
(x : αᵒᵖ) :
opposite.unop x⁻¹ = (opposite.unop x)⁻¹
@[simp]
theorem
opposite.op_sub
{α : Type u}
[add_group α]
(x y : α) :
opposite.op (x - y) = opposite.op x - opposite.op y
@[simp]
theorem
opposite.unop_sub
{α : Type u}
[add_group α]
(x y : αᵒᵖ) :
opposite.unop (x - y) = opposite.unop x - opposite.unop y
@[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
@[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
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' := _}
@[simp]
@[simp]
@[simp]
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)) :
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' := _}
@[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