Group structures on the multiplicative and additive opposites #

(Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun (x + y) = (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun x + (Equiv.trans (Equiv.neg G) AddOpposite.opEquiv).toFun y

source

@[simp]

theorem MulEquiv.inv'_symm_apply (G : Type u_2) [DivisionMonoid G] :

⇑(MulEquiv.inv' G).symm = Inv.inv ∘ MulOpposite.unop

source

@[simp]

theorem AddEquiv.neg'_apply (G : Type u_2) [SubtractionMonoid G] :

⇑(AddEquiv.neg' G) = AddOpposite.op ∘ Neg.neg

source

@[simp]

theorem AddEquiv.neg'_symm_apply (G : Type u_2) [SubtractionMonoid G] :

⇑(AddEquiv.neg' G).symm = Neg.neg ∘ AddOpposite.unop

source

@[simp]

theorem MulEquiv.inv'_apply (G : Type u_2) [DivisionMonoid G] :

⇑(MulEquiv.inv' G) = MulOpposite.op ∘ Inv.inv

source

def MulEquiv.inv' (G : Type u_2) [DivisionMonoid G] :

G ≃* Gᵐᵒᵖ

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

Equations

MulEquiv.inv' G = { toEquiv := Equiv.trans (Equiv.inv G) MulOpposite.opEquiv, map_mul' := ⋯ }

Instances For

source

def AddHom.toOpposite {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

AddHom M Nᵃᵒᵖ

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

Equations

f.toOpposite hf = { toFun := AddOpposite.op ∘ ⇑f, map_add' := ⋯ }

Instances For

source

theorem AddHom.toOpposite.proof_1 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) (x : M) (y : M) :

AddOpposite.op (f (x + y)) = AddOpposite.op (f x) + AddOpposite.op (f y)

source

@[simp]

theorem AddHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

⇑(f.toOpposite hf) = AddOpposite.op ∘ ⇑f

source

@[simp]

theorem MulHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f

source

def MulHom.toOpposite {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

M →ₙ* Nᵐᵒᵖ

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

f.toOpposite hf = { toFun := MulOpposite.op ∘ ⇑f, map_mul' := ⋯ }

Instances For

source

theorem AddHom.fromOpposite.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

∀ (x x_1 : Mᵃᵒᵖ), f (AddOpposite.unop x_1 + AddOpposite.unop x) = (⇑f ∘ AddOpposite.unop) x + (⇑f ∘ AddOpposite.unop) x_1

source

def AddHom.fromOpposite {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

AddHom Mᵃᵒᵖ N

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

Equations

f.fromOpposite hf = { toFun := ⇑f ∘ AddOpposite.unop, map_add' := ⋯ }

Instances For

source

@[simp]

theorem AddHom.fromOpposite_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

⇑(f.fromOpposite hf) = ⇑f ∘ AddOpposite.unop

source

@[simp]

theorem MulHom.fromOpposite_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop

source

def MulHom.fromOpposite {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

Mᵐᵒᵖ →ₙ* N

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

f.fromOpposite hf = { toFun := ⇑f ∘ MulOpposite.unop, map_mul' := ⋯ }

Instances For

source

def AddMonoidHom.toOpposite {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

M →+ Nᵃᵒᵖ

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

f.toOpposite hf = { toFun := AddOpposite.op ∘ ⇑f, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

theorem AddMonoidHom.toOpposite.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :

AddOpposite.op (f 0) = AddOpposite.op 0

source

theorem AddMonoidHom.toOpposite.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) (x : M) (y : M) :

AddOpposite.op (f (x + y)) = AddOpposite.op (f x) + AddOpposite.op (f y)

source

@[simp]

theorem AddMonoidHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

⇑(f.toOpposite hf) = AddOpposite.op ∘ ⇑f

source

@[simp]

theorem MonoidHom.toOpposite_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f

source

def MonoidHom.toOpposite {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

M →* Nᵐᵒᵖ

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

f.toOpposite hf = { toFun := MulOpposite.op ∘ ⇑f, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

def AddMonoidHom.fromOpposite {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

Mᵃᵒᵖ →+ N

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

f.fromOpposite hf = { toFun := ⇑f ∘ AddOpposite.unop, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

theorem AddMonoidHom.fromOpposite.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

∀ (x x_1 : Mᵃᵒᵖ), f (AddOpposite.unop x_1 + AddOpposite.unop x) = { toFun := ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }.toFun x + { toFun := ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }.toFun x_1

source

@[simp]

theorem AddMonoidHom.fromOpposite_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (hf : ∀ (x y : M), AddCommute (f x) (f y)) :

⇑(f.fromOpposite hf) = ⇑f ∘ AddOpposite.unop

source

@[simp]

theorem MonoidHom.fromOpposite_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop

source

def MonoidHom.fromOpposite {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) (hf : ∀ (x y : M), Commute (f x) (f y)) :

Mᵐᵒᵖ →* N

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

f.fromOpposite hf = { toFun := ⇑f ∘ MulOpposite.unop, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source

theorem AddUnits.opEquiv.proof_5 {M : Type u_1} [AddMonoid M] (x : AddUnits Mᵃᵒᵖ) :

(fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op ↑u, neg := AddOpposite.op ↑(-u), val_neg := ⋯, neg_val := ⋯ }) X) ((fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop ↑u, neg := AddOpposite.unop ↑(-u), val_neg := ⋯, neg_val := ⋯ }) x) = x

source

theorem AddUnits.opEquiv.proof_2 {M : Type u_1} [AddMonoid M] (u : AddUnits Mᵃᵒᵖ) :

AddOpposite.unop ↑(-u) + AddOpposite.unop ↑u = 0

source

theorem AddUnits.opEquiv.proof_1 {M : Type u_1} [AddMonoid M] (u : AddUnits Mᵃᵒᵖ) :

AddOpposite.unop ↑u + AddOpposite.unop ↑(-u) = 0

source

def AddUnits.opEquiv {M : Type u_2} [AddMonoid M] :

AddUnits Mᵃᵒᵖ ≃+ (AddUnits M)ᵃᵒᵖ

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem AddUnits.opEquiv.proof_4 {M : Type u_1} [AddMonoid M] (u : AddUnits M) :

AddOpposite.op ↑(-u) + AddOpposite.op ↑u = 0

source

theorem AddUnits.opEquiv.proof_6 {M : Type u_1} [AddMonoid M] (x : (AddUnits M)ᵃᵒᵖ) :

(fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop ↑u, neg := AddOpposite.unop ↑(-u), val_neg := ⋯, neg_val := ⋯ }) ((fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op ↑u, neg := AddOpposite.op ↑(-u), val_neg := ⋯, neg_val := ⋯ }) X) x) = x

source

theorem AddUnits.opEquiv.proof_7 {M : Type u_1} [AddMonoid M] :

∀ (x x_1 : AddUnits Mᵃᵒᵖ), { toFun := fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop ↑u, neg := AddOpposite.unop ↑(-u), val_neg := ⋯, neg_val := ⋯ }, invFun := fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op ↑u, neg := AddOpposite.op ↑(-u), val_neg := ⋯, neg_val := ⋯ }) X, left_inv := ⋯, right_inv := ⋯ }.toFun (x + x_1) = { toFun := fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop ↑u, neg := AddOpposite.unop ↑(-u), val_neg := ⋯, neg_val := ⋯ }, invFun := fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op ↑u, neg := AddOpposite.op ↑(-u), val_neg := ⋯, neg_val := ⋯ }) X, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := fun (u : AddUnits Mᵃᵒᵖ) => AddOpposite.op { val := AddOpposite.unop ↑u, neg := AddOpposite.unop ↑(-u), val_neg := ⋯, neg_val := ⋯ }, invFun := fun (X : (AddUnits M)ᵃᵒᵖ) => AddOpposite.rec' (fun (u : AddUnits M) => { val := AddOpposite.op ↑u, neg := AddOpposite.op ↑(-u), val_neg := ⋯, neg_val := ⋯ }) X, left_inv := ⋯, right_inv := ⋯ }.toFun x_1

source

theorem AddUnits.opEquiv.proof_3 {M : Type u_1} [AddMonoid M] (u : AddUnits M) :

AddOpposite.op ↑u + AddOpposite.op ↑(-u) = 0

source

def Units.opEquiv {M : Type u_2} [Monoid M] :

Mᵐᵒᵖˣ ≃* Mˣᵐᵒᵖ

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem AddUnits.coe_unop_opEquiv {M : Type u_2} [AddMonoid M] (u : AddUnits Mᵃᵒᵖ) :

↑(AddOpposite.unop (AddUnits.opEquiv u)) = AddOpposite.unop ↑u

source

@[simp]

theorem Units.coe_unop_opEquiv {M : Type u_2} [Monoid M] (u : Mᵐᵒᵖˣ) :

↑(MulOpposite.unop (Units.opEquiv u)) = MulOpposite.unop ↑u

source

@[simp]

theorem AddUnits.coe_opEquiv_symm {M : Type u_2} [AddMonoid M] (u : (AddUnits M)ᵃᵒᵖ) :

↑(AddUnits.opEquiv.symm u) = AddOpposite.op ↑(AddOpposite.unop u)

source

@[simp]

theorem Units.coe_opEquiv_symm {M : Type u_2} [Monoid M] (u : Mˣᵐᵒᵖ) :

↑(Units.opEquiv.symm u) = MulOpposite.op ↑(MulOpposite.unop u)

source

theorem IsAddUnit.op {M : Type u_2} [AddMonoid M] {m : M} (h : IsAddUnit m) :

IsAddUnit (AddOpposite.op m)

source

theorem IsUnit.op {M : Type u_2} [Monoid M] {m : M} (h : IsUnit m) :

IsUnit (MulOpposite.op m)

source

theorem IsAddUnit.unop {M : Type u_2} [AddMonoid M] {m : Mᵃᵒᵖ} (h : IsAddUnit m) :

IsAddUnit (AddOpposite.unop m)

source

theorem IsUnit.unop {M : Type u_2} [Monoid M] {m : Mᵐᵒᵖ} (h : IsUnit m) :

IsUnit (MulOpposite.unop m)

source

@[simp]

theorem isAddUnit_op {M : Type u_2} [AddMonoid M] {m : M} :

IsAddUnit (AddOpposite.op m) ↔ IsAddUnit m

source

@[simp]

theorem isUnit_op {M : Type u_2} [Monoid M] {m : M} :

IsUnit (MulOpposite.op m) ↔ IsUnit m

source

@[simp]

theorem isAddUnit_unop {M : Type u_2} [AddMonoid M] {m : Mᵃᵒᵖ} :

IsAddUnit (AddOpposite.unop m) ↔ IsAddUnit m

source

@[simp]

theorem isUnit_unop {M : Type u_2} [Monoid M] {m : Mᵐᵒᵖ} :

IsUnit (MulOpposite.unop m) ↔ IsUnit m

source

def AddHom.op {M : Type u_2} {N : Type u_3} [Add M] [Add N] :

AddHom M N ≃ AddHom Mᵃᵒᵖ Nᵃᵒᵖ

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem AddHom.op.proof_2 {M : Type u_2} {N : Type u_1} [Add M] [Add N] (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) (x : M) (y : M) :

AddOpposite.unop ((⇑f ∘ AddOpposite.op) (x + y)) = AddOpposite.unop { unop' := (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) x + (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) y }

source

theorem AddHom.op.proof_3 {M : Type u_1} {N : Type u_2} [Add M] [Add N] :

∀ (x : AddHom M N), (fun (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_add' := ⋯ }) ((fun (f : AddHom M N) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_add' := ⋯ }) x) = (fun (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_add' := ⋯ }) ((fun (f : AddHom M N) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_add' := ⋯ }) x)

source

theorem AddHom.op.proof_1 {M : Type u_1} {N : Type u_2} [Add M] [Add N] (f : AddHom M N) (x : Mᵃᵒᵖ) (y : Mᵃᵒᵖ) :

(AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) (x + y) = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) x + (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) y

source

theorem AddHom.op.proof_4 {M : Type u_1} {N : Type u_2} [Add M] [Add N] :

∀ (x : AddHom Mᵃᵒᵖ Nᵃᵒᵖ), (fun (f : AddHom M N) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_add' := ⋯ }) ((fun (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_add' := ⋯ }) x) = (fun (f : AddHom M N) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_add' := ⋯ }) ((fun (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_add' := ⋯ }) x)

source

@[simp]

theorem MulHom.op_apply_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : M →ₙ* N) :

∀ (a : Mᵐᵒᵖ), (MulHom.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

source

@[simp]

theorem MulHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] (f : Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) :

∀ (a : M), (MulHom.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

source

@[simp]

theorem AddHom.op_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) :

∀ (a : Mᵃᵒᵖ), (AddHom.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a

source

@[simp]

theorem AddHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom Mᵃᵒᵖ Nᵃᵒᵖ) :

∀ (a : M), (AddHom.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a

source

def MulHom.op {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] :

(M →ₙ* N) ≃ (Mᵐᵒᵖ →ₙ* 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

One or more equations did not get rendered due to their size.

Instances For

source

def AddHom.unop {M : Type u_2} {N : Type u_3} [Add M] [Add N] :

AddHom Mᵃᵒᵖ Nᵃᵒᵖ ≃ AddHom M N

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

Equations

AddHom.unop = AddHom.op.symm

Instances For

source

def MulHom.unop {M : Type u_2} {N : Type u_3} [Mul M] [Mul N] :

(Mᵐᵒᵖ →ₙ* Nᵐᵒᵖ) ≃ (M →ₙ* N)

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

Equations

MulHom.unop = MulHom.op.symm

Instances For

source

@[simp]

theorem AddHom.mulOp_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom M N) :

∀ (a : Mᵐᵒᵖ), (AddHom.mulOp f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

source

@[simp]

theorem AddHom.mulOp_symm_apply_apply {M : Type u_2} {N : Type u_3} [Add M] [Add N] (f : AddHom Mᵐᵒᵖ Nᵐᵒᵖ) :

∀ (a : M), (AddHom.mulOp.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

source

def AddHom.mulOp {M : Type u_2} {N : Type u_3} [Add M] [Add N] :

AddHom M N ≃ AddHom Mᵐᵒᵖ Nᵐᵒᵖ

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def AddHom.mulUnop {α : Type u_2} {β : Type u_3} [Add α] [Add β] :

AddHom αᵐᵒᵖ βᵐᵒᵖ ≃ AddHom α β

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

Equations

AddHom.mulUnop = AddHom.mulOp.symm

Instances For

source

theorem AddMonoidHom.op.proof_6 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

∀ (x : Mᵃᵒᵖ →+ Nᵃᵒᵖ), (fun (f : M →+ N) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯, map_add' := ⋯ }) ((fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_zero' := ⋯, map_add' := ⋯ }) x) = (fun (f : M →+ N) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯, map_add' := ⋯ }) ((fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_zero' := ⋯, map_add' := ⋯ }) x)

source

theorem AddMonoidHom.op.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (x : Mᵃᵒᵖ) (y : Mᵃᵒᵖ) :

{ toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }.toFun (x + y) = { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }.toFun x + { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯ }.toFun y

source

theorem AddMonoidHom.op.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :

AddOpposite.op ((⇑f ∘ AddOpposite.unop) 0) = AddOpposite.op 0

source

def AddMonoidHom.op {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] :

(M →+ N) ≃ (Mᵃᵒᵖ →+ Nᵃᵒᵖ)

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

One or more equations did not get rendered due to their size.

Instances For

source

theorem AddMonoidHom.op.proof_3 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) :

AddOpposite.unop ((⇑f ∘ AddOpposite.op) 0) = AddOpposite.unop { unop' := 0 }

source

theorem AddMonoidHom.op.proof_4 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) (x : M) (y : M) :

AddOpposite.unop { unop' := (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) (x + y) } = AddOpposite.unop { unop' := { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_zero' := ⋯ }.toFun x + { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_zero' := ⋯ }.toFun y }

source

theorem AddMonoidHom.op.proof_5 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

∀ (x : M →+ N), (fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_zero' := ⋯, map_add' := ⋯ }) ((fun (f : M →+ N) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯, map_add' := ⋯ }) x) = (fun (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_zero' := ⋯, map_add' := ⋯ }) ((fun (f : M →+ N) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯, map_add' := ⋯ }) x)

source

@[simp]

theorem MonoidHom.op_apply_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : M →* N) :

∀ (a : Mᵐᵒᵖ), (MonoidHom.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

source

@[simp]

theorem AddMonoidHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : Mᵃᵒᵖ →+ Nᵃᵒᵖ) :

∀ (a : M), (AddMonoidHom.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a

source

@[simp]

theorem MonoidHom.op_symm_apply_apply {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] (f : Mᵐᵒᵖ →* Nᵐᵒᵖ) :

∀ (a : M), (MonoidHom.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

source

@[simp]

theorem AddMonoidHom.op_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :

∀ (a : Mᵃᵒᵖ), (AddMonoidHom.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a

source

def MonoidHom.op {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] :

(M →* N) ≃ (Mᵐᵒᵖ →* Nᵐᵒᵖ)

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

One or more equations did not get rendered due to their size.

Instances For

source

def AddMonoidHom.unop {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] :

(Mᵃᵒᵖ →+ Nᵃᵒᵖ) ≃ (M →+ N)

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

Equations

AddMonoidHom.unop = AddMonoidHom.op.symm

Instances For

source

def MonoidHom.unop {M : Type u_2} {N : Type u_3} [MulOneClass M] [MulOneClass N] :

(Mᵐᵒᵖ →* Nᵐᵒᵖ) ≃ (M →* N)

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

Equations

MonoidHom.unop = MonoidHom.op.symm

Instances For

source

theorem AddEquiv.opOp.proof_1 (M : Type u_1) [Add M] :

∀ (x x_1 : M), (AddOpposite.opEquiv.trans AddOpposite.opEquiv).toFun (x + x_1) = (AddOpposite.opEquiv.trans AddOpposite.opEquiv).toFun (x + x_1)

source

def AddEquiv.opOp (M : Type u_2) [Add M] :

M ≃+ Mᵃᵒᵖᵃᵒᵖ

A additive monoid is isomorphic to the opposite of its opposite.

Equations

AddEquiv.opOp M = { toEquiv := AddOpposite.opEquiv.trans AddOpposite.opEquiv, map_add' := ⋯ }

Instances For

source

@[simp]

theorem MulEquiv.opOp_apply (M : Type u_2) [Mul M] :

∀ (a : M), (MulEquiv.opOp M) a = MulOpposite.op (MulOpposite.op a)

source

@[simp]

theorem AddEquiv.opOp_symm_apply (M : Type u_2) [Add M] :

∀ (a : Mᵃᵒᵖᵃᵒᵖ), (AddEquiv.opOp M).symm a = AddOpposite.unop (AddOpposite.unop a)

source

@[simp]

theorem AddEquiv.opOp_apply (M : Type u_2) [Add M] :

∀ (a : M), (AddEquiv.opOp M) a = AddOpposite.op (AddOpposite.op a)

source

@[simp]

theorem MulEquiv.opOp_symm_apply (M : Type u_2) [Mul M] :

∀ (a : Mᵐᵒᵖᵐᵒᵖ), (MulEquiv.opOp M).symm a = MulOpposite.unop (MulOpposite.unop a)

source

def MulEquiv.opOp (M : Type u_2) [Mul M] :

M ≃* Mᵐᵒᵖᵐᵒᵖ

A monoid is isomorphic to the opposite of its opposite.

Equations

MulEquiv.opOp M = { toEquiv := MulOpposite.opEquiv.trans MulOpposite.opEquiv, map_mul' := ⋯ }

Instances For

source

@[simp]

theorem AddMonoidHom.mulOp_symm_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : Mᵐᵒᵖ →+ Nᵐᵒᵖ) :

∀ (a : M), (AddMonoidHom.mulOp.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

source

@[simp]

theorem AddMonoidHom.mulOp_apply_apply {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) :

∀ (a : Mᵐᵒᵖ), (AddMonoidHom.mulOp f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

source

def AddMonoidHom.mulOp {M : Type u_2} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] :

(M →+ N) ≃ (Mᵐᵒᵖ →+ Nᵐᵒᵖ)

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

One or more equations did not get rendered due to their size.

Instances For

source

def AddMonoidHom.mulUnop {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] :

(αᵐᵒᵖ →+ βᵐᵒᵖ) ≃ (α →+ β)

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

Equations

AddMonoidHom.mulUnop = AddMonoidHom.mulOp.symm

Instances For

source

@[simp]

theorem AddEquiv.mulOp_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) :

AddEquiv.mulOp f = MulOpposite.opAddEquiv.symm.trans (f.trans MulOpposite.opAddEquiv)

source

@[simp]

theorem AddEquiv.mulOp_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵐᵒᵖ ≃+ βᵐᵒᵖ) :

AddEquiv.mulOp.symm f = MulOpposite.opAddEquiv.trans (f.trans MulOpposite.opAddEquiv.symm)

source

def AddEquiv.mulOp {α : Type u_2} {β : Type u_3} [Add α] [Add β] :

α ≃+ β ≃ (αᵐᵒᵖ ≃+ βᵐᵒᵖ)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def AddEquiv.mulUnop {α : Type u_2} {β : Type u_3} [Add α] [Add β] :

αᵐᵒᵖ ≃+ βᵐᵒᵖ ≃ (α ≃+ β)

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

Equations

AddEquiv.mulUnop = AddEquiv.mulOp.symm

Instances For

source

def AddEquiv.op {α : Type u_2} {β : Type u_3} [Add α] [Add β] :

α ≃+ β ≃ (αᵃᵒᵖ ≃+ βᵃᵒᵖ)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem AddEquiv.op.proof_8 {α : Type u_1} {β : Type u_2} [Add α] [Add β] :

∀ (x : αᵃᵒᵖ ≃+ βᵃᵒᵖ), (fun (f : α ≃+ β) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }) ((fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ⇑f.symm ∘ AddOpposite.op, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }) x) = (fun (f : α ≃+ β) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }) ((fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ⇑f.symm ∘ AddOpposite.op, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }) x)

source

theorem AddEquiv.op.proof_1 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : α ≃+ β) (x : αᵃᵒᵖ) :

(AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop) ((AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) x) = x

source

theorem AddEquiv.op.proof_2 {α : Type u_2} {β : Type u_1} [Add α] [Add β] (f : α ≃+ β) (x : βᵃᵒᵖ) :

(AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) ((AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop) x) = x

source

theorem AddEquiv.op.proof_5 {α : Type u_2} {β : Type u_1} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (x : β) :

AddOpposite.unop (f (f.symm (AddOpposite.op x))) = x

source

theorem AddEquiv.op.proof_4 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (x : α) :

AddOpposite.unop (f.symm (f (AddOpposite.op x))) = x

source

theorem AddEquiv.op.proof_7 {α : Type u_1} {β : Type u_2} [Add α] [Add β] :

∀ (x : α ≃+ β), (fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ⇑f.symm ∘ AddOpposite.op, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }) ((fun (f : α ≃+ β) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }) x) = (fun (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ⇑f.symm ∘ AddOpposite.op, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }) ((fun (f : α ≃+ β) => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }) x)

source

theorem AddEquiv.op.proof_3 {α : Type u_1} {β : Type u_2} [Add α] [Add β] (f : α ≃+ β) (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) :

{ toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯ }.toFun (x + y) = { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, invFun := AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop, left_inv := ⋯, right_inv := ⋯ }.toFun y

source

theorem AddEquiv.op.proof_6 {α : Type u_2} {β : Type u_1} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) (x : α) (y : α) :

AddOpposite.unop { unop' := (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) (x + y) } = AddOpposite.unop { unop' := { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ⇑f.symm ∘ AddOpposite.op, left_inv := ⋯, right_inv := ⋯ }.toFun x + { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, invFun := AddOpposite.unop ∘ ⇑f.symm ∘ AddOpposite.op, left_inv := ⋯, right_inv := ⋯ }.toFun y }

source

@[simp]

theorem AddEquiv.op_symm_apply_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) :

∀ (a : β), (AddEquiv.op.symm f).symm a = (AddOpposite.unop ∘ ⇑f.symm ∘ AddOpposite.op) a

source

@[simp]

theorem MulEquiv.op_apply_symm_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : α ≃* β) :

∀ (a : βᵐᵒᵖ), (MulEquiv.op f).symm a = (MulOpposite.op ∘ ⇑f.symm ∘ MulOpposite.unop) a

source

@[simp]

theorem AddEquiv.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : αᵃᵒᵖ ≃+ βᵃᵒᵖ) :

∀ (a : α), (AddEquiv.op.symm f) a = (AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op) a

source

@[simp]

theorem MulEquiv.op_symm_apply_symm_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) :

∀ (a : β), (MulEquiv.op.symm f).symm a = (MulOpposite.unop ∘ ⇑f.symm ∘ MulOpposite.op) a

source

@[simp]

theorem AddEquiv.op_apply_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) :

∀ (a : αᵃᵒᵖ), (AddEquiv.op f) a = (AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop) a

source

@[simp]

theorem AddEquiv.op_apply_symm_apply {α : Type u_2} {β : Type u_3} [Add α] [Add β] (f : α ≃+ β) :

∀ (a : βᵃᵒᵖ), (AddEquiv.op f).symm a = (AddOpposite.op ∘ ⇑f.symm ∘ AddOpposite.unop) a

source

@[simp]

theorem MulEquiv.op_apply_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : α ≃* β) :

∀ (a : αᵐᵒᵖ), (MulEquiv.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a

source

@[simp]

theorem MulEquiv.op_symm_apply_apply {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] (f : αᵐᵒᵖ ≃* βᵐᵒᵖ) :

∀ (a : α), (MulEquiv.op.symm f) a = (MulOpposite.unop ∘ ⇑f ∘ MulOpposite.op) a

source

def MulEquiv.op {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] :

α ≃* β ≃ (αᵐᵒᵖ ≃* βᵐᵒᵖ)

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

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def AddEquiv.unop {α : Type u_2} {β : Type u_3} [Add α] [Add β] :

αᵃᵒᵖ ≃+ βᵃᵒᵖ ≃ (α ≃+ β)

The 'unopposite' of an iso αᵃᵒᵖ ≃+ βᵃᵒᵖ. Inverse to AddEquiv.op.

Equations

AddEquiv.unop = AddEquiv.op.symm

Instances For

source

def MulEquiv.unop {α : Type u_2} {β : Type u_3} [Mul α] [Mul β] :

αᵐᵒᵖ ≃* βᵐᵒᵖ ≃ (α ≃* β)

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

Equations

MulEquiv.unop = MulEquiv.op.symm

Instances For

source

theorem AddMonoidHom.mul_op_ext_iff {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] {f : αᵐᵒᵖ →+ β} {g : αᵐᵒᵖ →+ β} :

f = g ↔ f.comp MulOpposite.opAddEquiv.toAddMonoidHom = g.comp MulOpposite.opAddEquiv.toAddMonoidHom

source

theorem AddMonoidHom.mul_op_ext {α : Type u_2} {β : Type u_3} [AddZeroClass α] [AddZeroClass β] (f : αᵐᵒᵖ →+ β) (g : αᵐᵒᵖ →+ β) (h : f.comp MulOpposite.opAddEquiv.toAddMonoidHom = g.comp MulOpposite.opAddEquiv.toAddMonoidHom) :

f = g

This ext lemma changes 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.addHom_ext'.

HepLean Documentation

Mathlib.Algebra.Group.Opposite

Group structures on the multiplicative and additive opposites #

Additive structures on `αᵐᵒᵖ` #

Multiplicative structures on `αᵐᵒᵖ` #

Multiplicative structures on `αᵃᵒᵖ` #

Group structures on the multiplicative and additive opposites #

Additive structures on αᵐᵒᵖ #

Multiplicative structures on αᵐᵒᵖ #

Multiplicative structures on αᵃᵒᵖ #

Additive structures on `αᵐᵒᵖ` #

Multiplicative structures on `αᵐᵒᵖ` #

Multiplicative structures on `αᵃᵒᵖ` #