# mathlibdocumentation

algebra.group.opposite

# Group structures on the multiplicative and additive opposites #

### Additive structures on αᵐᵒᵖ#

@[protected, instance]
def mul_opposite.add_semigroup (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.add_comm_semigroup (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.add_zero_class (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.add_monoid_with_one (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.add_comm_monoid (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.sub_neg_monoid (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.add_group_with_one (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.add_comm_group (α : Type u)  :
Equations

### Multiplicative structures on αᵐᵒᵖ#

We also generate additive structures on αᵃᵒᵖ using to_additive

@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.semigroup (α : Type u) [semigroup α] :
Equations
@[protected, instance]
def mul_opposite.left_cancel_semigroup (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.right_cancel_semigroup (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.comm_semigroup (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.mul_one_class (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.monoid (α : Type u) [monoid α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.left_cancel_monoid (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.right_cancel_monoid (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.cancel_monoid (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.comm_monoid (α : Type u) [comm_monoid α] :
Equations
@[protected, instance]
def mul_opposite.cancel_comm_monoid (α : Type u)  :
Equations
@[protected, instance]
Equations
@[protected, instance]
def add_opposite.sub_neg_monoid (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.div_inv_monoid (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.subtraction_monoid (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.division_monoid (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.division_comm_monoid (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.subtraction_comm_monoid (α : Type u)  :
Equations
@[protected, instance]
def mul_opposite.group (α : Type u) [group α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def mul_opposite.comm_group (α : Type u) [comm_group α] :
Equations
@[protected, instance]
Equations
@[simp]
theorem add_opposite.unop_sub {α : Type u} (x y : αᵃᵒᵖ) :
@[simp]
theorem mul_opposite.unop_div {α : Type u} (x y : αᵐᵒᵖ) :
@[simp]
theorem add_opposite.op_sub {α : Type u} (x y : α) :
@[simp]
theorem mul_opposite.op_div {α : Type u} (x y : α) :
@[simp]
theorem add_opposite.semiconj_by_op {α : Type u} [has_add α] {a x y : α} :
y
@[simp]
theorem mul_opposite.semiconj_by_op {α : Type u} [has_mul α] {a x y : α} :
x y
@[simp]
theorem add_opposite.semiconj_by_unop {α : Type u} [has_add α] {a x y : αᵃᵒᵖ} :
y
@[simp]
theorem mul_opposite.semiconj_by_unop {α : Type u} [has_mul α] {a x y : αᵐᵒᵖ} :
x y
theorem semiconj_by.op {α : Type u} [has_mul α] {a x y : α} (h : x y) :
theorem add_semiconj_by.op {α : Type u} [has_add α] {a x y : α} (h : y) :
theorem semiconj_by.unop {α : Type u} [has_mul α] {a x y : αᵐᵒᵖ} (h : x y) :
theorem add_semiconj_by.unop {α : Type u} [has_add α] {a x y : αᵃᵒᵖ} (h : y) :
theorem commute.op {α : Type u} [has_mul α] {x y : α} (h : y) :
theorem add_commute.op {α : Type u} [has_add α] {x y : α} (h : y) :
theorem add_opposite.commute.unop {α : Type u} [has_add α] {x y : αᵃᵒᵖ} (h : y) :
theorem mul_opposite.commute.unop {α : Type u} [has_mul α] {x y : αᵐᵒᵖ} (h : y) :
@[simp]
theorem add_opposite.commute_op {α : Type u} [has_add α] {x y : α} :
y
@[simp]
theorem mul_opposite.commute_op {α : Type u} [has_mul α] {x y : α} :
y
@[simp]
theorem mul_opposite.commute_unop {α : Type u} [has_mul α] {x y : αᵐᵒᵖ} :
y
@[simp]
theorem add_opposite.commute_unop {α : Type u} [has_add α] {x y : αᵃᵒᵖ} :
@[simp]

The function mul_opposite.op is an additive equivalence.

Equations
@[simp]
@[simp]

### Multiplicative structures on αᵃᵒᵖ#

@[protected, instance]
def add_opposite.semigroup (α : Type u) [semigroup α] :
Equations
@[protected, instance]
def add_opposite.left_cancel_semigroup (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.right_cancel_semigroup (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.comm_semigroup (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.mul_one_class (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.has_pow (α : Type u) {β : Type u_1} [ β] :
β
Equations
@[simp]
theorem add_opposite.op_pow (α : Type u) {β : Type u_1} [ β] (a : α) (b : β) :
@[simp]
theorem add_opposite.unop_pow (α : Type u) {β : Type u_1} [ β] (a : αᵃᵒᵖ) (b : β) :
@[protected, instance]
def add_opposite.monoid (α : Type u) [monoid α] :
Equations
@[protected, instance]
def add_opposite.comm_monoid (α : Type u) [comm_monoid α] :
Equations
@[protected, instance]
def add_opposite.div_inv_monoid (α : Type u)  :
Equations
@[protected, instance]
def add_opposite.group (α : Type u) [group α] :
Equations
@[protected, instance]
def add_opposite.comm_group (α : Type u) [comm_group α] :
Equations
@[simp]
theorem add_opposite.op_mul_equiv_apply {α : Type u} [has_mul α] :
@[simp]
theorem add_opposite.op_mul_equiv_symm_apply {α : Type u} [has_mul α] :
def add_opposite.op_mul_equiv {α : Type u} [has_mul α] :

The function add_opposite.op is a multiplicative equivalence.

Equations
@[simp]
theorem add_opposite.op_mul_equiv_to_equiv {α : Type u} [has_mul α] :
@[simp]
theorem add_equiv.neg'_symm_apply (G : Type u_1)  :
@[simp]
theorem mul_equiv.inv'_symm_apply (G : Type u_1)  :
def add_equiv.neg' (G : Type u_1)  :

Negation on an additive group is an add_equiv to the opposite group. When G is commutative, there is add_equiv.inv.

Equations
@[simp]
theorem add_equiv.neg'_apply (G : Type u_1)  :
@[simp]
theorem mul_equiv.inv'_apply (G : Type u_1)  :
def mul_equiv.inv' (G : Type u_1)  :

Inversion on a group is a mul_equiv to the opposite group. When G is commutative, there is mul_equiv.inv.

Equations
@[simp]
theorem mul_hom.to_opposite_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), commute (f x) (f y)) :
def add_hom.to_opposite {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) (hf : ∀ (x y : M), add_commute (f x) (f y)) :

An additive semigroup homomorphism f : add_hom M N such that f x additively commutes with f y for all x, y defines an additive semigroup homomorphism to Sᵃᵒᵖ.

Equations
@[simp]
theorem add_hom.to_opposite_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) (hf : ∀ (x y : M), add_commute (f x) (f y)) :
def mul_hom.to_opposite {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), commute (f x) (f y)) :

A semigroup homomorphism f : M →ₙ* N such that f x commutes with f y for all x, y defines a semigroup homomorphism to Nᵐᵒᵖ.

Equations
def add_hom.from_opposite {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) (hf : ∀ (x y : M), add_commute (f x) (f y)) :
N

An additive semigroup homomorphism f : add_hom M N such that f x additively commutes with f y for all x, y defines an additive semigroup homomorphism from Mᵃᵒᵖ.

Equations
@[simp]
theorem add_hom.from_opposite_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) (hf : ∀ (x y : M), add_commute (f x) (f y)) :
@[simp]
theorem mul_hom.from_opposite_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), commute (f x) (f y)) :
def mul_hom.from_opposite {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), commute (f x) (f y)) :

A semigroup homomorphism f : M →ₙ* N such that f x commutes with f y for all x, y defines a semigroup homomorphism from Mᵐᵒᵖ.

Equations
@[simp]
theorem add_monoid_hom.to_opposite_apply {M : Type u_1} {N : Type u_2} (f : M →+ N) (hf : ∀ (x y : M), add_commute (f x) (f y)) :
def add_monoid_hom.to_opposite {M : Type u_1} {N : Type u_2} (f : M →+ N) (hf : ∀ (x y : M), add_commute (f x) (f y)) :

An additive monoid homomorphism f : M →+ N such that f x additively commutes with f y for all x, y defines an additive monoid homomorphism to Sᵃᵒᵖ.

Equations
@[simp]
theorem monoid_hom.to_opposite_apply {M : Type u_1} {N : Type u_2} (f : M →* N) (hf : ∀ (x y : M), commute (f x) (f y)) :
def monoid_hom.to_opposite {M : Type u_1} {N : Type u_2} (f : M →* N) (hf : ∀ (x y : M), commute (f x) (f y)) :

A monoid homomorphism f : M →* N such that f x commutes with f y for all x, y defines a monoid homomorphism to Nᵐᵒᵖ.

Equations
def add_monoid_hom.from_opposite {M : Type u_1} {N : Type u_2} (f : M →+ N) (hf : ∀ (x y : M), add_commute (f x) (f y)) :

An additive monoid homomorphism f : M →+ N such that f x additively commutes with f y for all x, y defines an additive monoid homomorphism from Mᵃᵒᵖ.

Equations
@[simp]
theorem add_monoid_hom.from_opposite_apply {M : Type u_1} {N : Type u_2} (f : M →+ N) (hf : ∀ (x y : M), add_commute (f x) (f y)) :
def monoid_hom.from_opposite {M : Type u_1} {N : Type u_2} (f : M →* N) (hf : ∀ (x y : M), commute (f x) (f y)) :

A monoid homomorphism f : M →* N such that f x commutes with f y for all x, y defines a monoid homomorphism from Mᵐᵒᵖ.

Equations
@[simp]
theorem monoid_hom.from_opposite_apply {M : Type u_1} {N : Type u_2} (f : M →* N) (hf : ∀ (x y : M), commute (f x) (f y)) :

Equations
def units.op_equiv {M : Type u_1} [monoid M] :

The units of the opposites are equivalent to the opposites of the units.

Equations
@[simp]
@[simp]
theorem units.coe_unop_op_equiv {M : Type u_1} [monoid M] (u : Mᵐᵒᵖˣ) :
@[simp]
@[simp]
theorem units.coe_op_equiv_symm {M : Type u_1} [monoid M] (u : Mˣᵐᵒᵖ) :
@[simp]
theorem add_hom.op_apply_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) (ᾰ : Mᵃᵒᵖ) :
@[simp]
theorem mul_hom.op_symm_apply_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) (ᾰ : M) :
N

An additive semigroup homomorphism add_hom M N can equivalently be viewed as an additive semigroup homomorphism add_hom Mᵃᵒᵖ Nᵃᵒᵖ. This is the action of the (fully faithful) ᵃᵒᵖ-functor on morphisms.

Equations
def mul_hom.op {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :

A semigroup homomorphism M →ₙ* N can equivalently be viewed as a semigroup homomorphism Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations
@[simp]
theorem mul_hom.op_apply_apply {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] (f : M →ₙ* N) (ᾰ : Mᵐᵒᵖ) :
@[simp]
theorem add_hom.op_symm_apply_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : Nᵃᵒᵖ) (ᾰ : M) :
@[simp]
def mul_hom.unop {M : Type u_1} {N : Type u_2} [has_mul M] [has_mul N] :

The 'unopposite' of a semigroup homomorphism Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ. Inverse to mul_hom.op.

Equations
@[simp]
N

The 'unopposite' of an additive semigroup homomorphism Mᵃᵒᵖ →ₙ+ Nᵃᵒᵖ. Inverse to add_hom.op.

Equations
@[simp]
theorem add_hom.mul_op_apply_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : N) (ᾰ : Mᵐᵒᵖ) :
=
@[simp]
theorem add_hom.mul_op_symm_apply_apply {M : Type u_1} {N : Type u_2} [has_add M] [has_add N] (f : Nᵐᵒᵖ) (ᾰ : M) :
N

An additive semigroup homomorphism add_hom M N can equivalently be viewed as an additive homomorphism add_hom Mᵐᵒᵖ Nᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations
@[simp]
β

The 'unopposite' of an additive semigroup hom αᵐᵒᵖ →+ βᵐᵒᵖ. Inverse to add_hom.mul_op.

Equations
def add_monoid_hom.op {M : Type u_1} {N : Type u_2}  :

An additive monoid homomorphism M →+ N can equivalently be viewed as an additive monoid homomorphism Mᵃᵒᵖ →+ Nᵃᵒᵖ. This is the action of the (fully faithful) ᵃᵒᵖ-functor on morphisms.

Equations
def monoid_hom.op {M : Type u_1} {N : Type u_2}  :

A monoid homomorphism M →* N can equivalently be viewed as a monoid homomorphism Mᵐᵒᵖ →* Nᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations
@[simp]
theorem monoid_hom.op_apply_apply {M : Type u_1} {N : Type u_2} (f : M →* N) (ᾰ : Mᵐᵒᵖ) :
=
@[simp]
theorem monoid_hom.op_symm_apply_apply {M : Type u_1} {N : Type u_2} (f : Mᵐᵒᵖ →* Nᵐᵒᵖ) (ᾰ : M) :
@[simp]
theorem add_monoid_hom.op_apply_apply {M : Type u_1} {N : Type u_2} (f : M →+ N) (ᾰ : Mᵃᵒᵖ) :
=
@[simp]
theorem add_monoid_hom.op_symm_apply_apply {M : Type u_1} {N : Type u_2} (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) (ᾰ : M) :
@[simp]
def add_monoid_hom.unop {M : Type u_1} {N : Type u_2}  :

The 'unopposite' of an additive monoid homomorphism Mᵃᵒᵖ →+ Nᵃᵒᵖ. Inverse to add_monoid_hom.op.

Equations
@[simp]
def monoid_hom.unop {M : Type u_1} {N : Type u_2}  :

The 'unopposite' of a monoid homomorphism Mᵐᵒᵖ →* Nᵐᵒᵖ. Inverse to monoid_hom.op.

Equations
def add_monoid_hom.mul_op {M : Type u_1} {N : Type u_2}  :

An additive homomorphism M →+ N can equivalently be viewed as an additive homomorphism Mᵐᵒᵖ →+ Nᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations
@[simp]
theorem add_monoid_hom.mul_op_symm_apply_apply {M : Type u_1} {N : Type u_2} (f : Mᵐᵒᵖ →+ Nᵐᵒᵖ) (ᾰ : M) :
@[simp]
theorem add_monoid_hom.mul_op_apply_apply {M : Type u_1} {N : Type u_2} (f : M →+ N) (ᾰ : Mᵐᵒᵖ) :
=
@[simp]
def add_monoid_hom.mul_unop {α : Type u_1} {β : Type u_2}  :

The 'unopposite' of an additive monoid hom αᵐᵒᵖ →+ βᵐᵒᵖ. Inverse to add_monoid_hom.mul_op.

Equations
@[simp]
theorem add_equiv.mul_op_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : α ≃+ β) :
@[simp]
theorem add_equiv.mul_op_symm_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : αᵐᵒᵖ ≃+ βᵐᵒᵖ) :

A iso α ≃+ β can equivalently be viewed as an iso αᵐᵒᵖ ≃+ βᵐᵒᵖ.

Equations
@[simp]

The 'unopposite' of an iso αᵐᵒᵖ ≃+ βᵐᵒᵖ. Inverse to add_equiv.mul_op.

Equations
@[simp]
theorem add_equiv.op_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (ᾰ : β) :
@[simp]
theorem mul_equiv.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) (ᾰ : α) :
@[simp]
theorem mul_equiv.op_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) (ᾰ : β) :
(((mul_equiv.op.symm) f).symm) =

A iso α ≃+ β can equivalently be viewed as an iso αᵃᵒᵖ ≃+ βᵃᵒᵖ.

Equations
@[simp]
theorem add_equiv.op_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : α ≃+ β) (ᾰ : βᵃᵒᵖ) :
@[simp]
theorem add_equiv.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (ᾰ : α) :
def mul_equiv.op {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] :

A iso α ≃* β can equivalently be viewed as an iso αᵐᵒᵖ ≃* βᵐᵒᵖ.

Equations
@[simp]
theorem mul_equiv.op_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : α ≃* β) (ᾰ : βᵐᵒᵖ) :
((mul_equiv.op f).symm) =
@[simp]
theorem mul_equiv.op_apply_apply {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] (f : α ≃* β) (ᾰ : αᵐᵒᵖ) :
=
@[simp]
theorem add_equiv.op_apply_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_add β] (f : α ≃+ β) (ᾰ : αᵃᵒᵖ) :
=
@[simp]
def mul_equiv.unop {α : Type u_1} {β : Type u_2} [has_mul α] [has_mul β] :

The 'unopposite' of an iso αᵐᵒᵖ ≃* βᵐᵒᵖ. Inverse to mul_equiv.op.

Equations
@[simp]
The 'unopposite' of an iso αᵃᵒᵖ ≃+ βᵃᵒᵖ. Inverse to add_equiv.op.
This ext lemma change equalities on αᵐᵒᵖ →+ β to equalities on α →+ β. This is useful because there are often ext lemmas for specific αs that will apply to an equality of α →+ β such as finsupp.add_hom_ext'.