Ring structures on the multiplicative opposite

instance MulOpposite.instDistrib (α : Type u) [Distrib α] : Distrib αᵐᵒᵖ

Equations

• MulOpposite.instDistrib α = let __src := MulOpposite.add α; let __src_1 := MulOpposite.mul α; Distrib.mk ⋯ ⋯

instance MulOpposite.instMulZeroClass (α : Type u) [MulZeroClass α] : MulZeroClass αᵐᵒᵖ

Equations

• MulOpposite.instMulZeroClass α = MulZeroClass.mk ⋯ ⋯

instance MulOpposite.instMulZeroOneClass (α : Type u) [MulZeroOneClass α] : MulZeroOneClass αᵐᵒᵖ

Equations

• MulOpposite.instMulZeroOneClass α = let __src := MulOpposite.instMulZeroClass α; let __src_1 := MulOpposite.mulOneClass α; MulZeroOneClass.mk ⋯ ⋯

instance MulOpposite.instSemigroupWithZero (α : Type u) [SemigroupWithZero α] : SemigroupWithZero αᵐᵒᵖ

Equations

• MulOpposite.instSemigroupWithZero α = let __src := MulOpposite.semigroup α; let __src_1 := MulOpposite.instMulZeroClass α; SemigroupWithZero.mk ⋯ ⋯

instance MulOpposite.instMonoidWithZero (α : Type u) [MonoidWithZero α] : MonoidWithZero αᵐᵒᵖ

Equations

• MulOpposite.instMonoidWithZero α = let __src := MulOpposite.monoid α; let __src_1 := MulOpposite.instMulZeroOneClass α; MonoidWithZero.mk ⋯ ⋯

instance MulOpposite.instNonUnitalNonAssocSemiring (α : Type u) [NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring αᵐᵒᵖ

Equations

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

instance MulOpposite.instNonUnitalSemiring (α : Type u) [NonUnitalSemiring α] : NonUnitalSemiring αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalSemiring α = let __src := MulOpposite.instSemigroupWithZero α; let __src_1 := MulOpposite.instNonUnitalNonAssocSemiring α; NonUnitalSemiring.mk ⋯

instance MulOpposite.instNonAssocSemiring (α : Type u) [NonAssocSemiring α] : NonAssocSemiring αᵐᵒᵖ

Equations

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

instance MulOpposite.instSemiring (α : Type u) [Semiring α] : Semiring αᵐᵒᵖ

Equations

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

instance MulOpposite.instNonUnitalCommSemiring (α : Type u) [NonUnitalCommSemiring α] : NonUnitalCommSemiring αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalCommSemiring α = let __src := MulOpposite.instNonUnitalSemiring α; let __src_1 := MulOpposite.commSemigroup α; NonUnitalCommSemiring.mk ⋯

instance MulOpposite.instCommSemiring (α : Type u) [CommSemiring α] : CommSemiring αᵐᵒᵖ

Equations

• MulOpposite.instCommSemiring α = let __src := MulOpposite.instSemiring α; let __src_1 := MulOpposite.commSemigroup α; CommSemiring.mk ⋯

instance MulOpposite.instNonUnitalNonAssocRing (α : Type u) [NonUnitalNonAssocRing α] : NonUnitalNonAssocRing αᵐᵒᵖ

Equations

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

instance MulOpposite.instNonUnitalRing (α : Type u) [NonUnitalRing α] : NonUnitalRing αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalRing α = let __src := MulOpposite.addCommGroup α; let __src_1 := MulOpposite.instSemigroupWithZero α; let __src_2 := MulOpposite.instDistrib α; NonUnitalRing.mk ⋯

instance MulOpposite.instNonAssocRing (α : Type u) [NonAssocRing α] : NonAssocRing αᵐᵒᵖ

Equations

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

instance MulOpposite.instRing (α : Type u) [Ring α] : Ring αᵐᵒᵖ

Equations

• MulOpposite.instRing α = let __src := MulOpposite.monoid α; let __src_1 := MulOpposite.instNonAssocRing α; Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance MulOpposite.instNonUnitalCommRing (α : Type u) [NonUnitalCommRing α] : NonUnitalCommRing αᵐᵒᵖ

Equations

• MulOpposite.instNonUnitalCommRing α = let __src := MulOpposite.instNonUnitalRing α; let __src_1 := MulOpposite.instNonUnitalCommSemiring α; NonUnitalCommRing.mk ⋯

instance MulOpposite.instCommRing (α : Type u) [CommRing α] : CommRing αᵐᵒᵖ

Equations

• MulOpposite.instCommRing α = let __src := MulOpposite.instRing α; let __src_1 := MulOpposite.instCommSemiring α; CommRing.mk ⋯

instance MulOpposite.instNoZeroDivisors (α : Type u) [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵐᵒᵖ

Equations

• ⋯ = ⋯

instance MulOpposite.instIsDomain (α : Type u) [Ring α] [IsDomain α] : IsDomain αᵐᵒᵖ

Equations

• ⋯ = ⋯

instance MulOpposite.instGroupWithZero (α : Type u) [GroupWithZero α] : GroupWithZero αᵐᵒᵖ

Equations

• MulOpposite.instGroupWithZero α = let __src := MulOpposite.instMonoidWithZero α; let __src_1 := MulOpposite.divInvMonoid α; let __src_2 := ⋯; GroupWithZero.mk ⋯ DivInvMonoid.zpow ⋯ ⋯ ⋯ ⋯ ⋯

instance AddOpposite.instDistrib (α : Type u) [Distrib α] : Distrib αᵃᵒᵖ

Equations

• AddOpposite.instDistrib α = let __src := AddOpposite.add α; let __src_1 := AddOpposite.mul; Distrib.mk ⋯ ⋯

instance AddOpposite.instMulZeroClass (α : Type u) [MulZeroClass α] : MulZeroClass αᵃᵒᵖ

Equations

• AddOpposite.instMulZeroClass α = MulZeroClass.mk ⋯ ⋯

instance AddOpposite.instMulZeroOneClass (α : Type u) [MulZeroOneClass α] : MulZeroOneClass αᵃᵒᵖ

Equations

• AddOpposite.instMulZeroOneClass α = let __src := AddOpposite.instMulZeroClass α; let __src_1 := AddOpposite.mulOneClass α; MulZeroOneClass.mk ⋯ ⋯

instance AddOpposite.instSemigroupWithZero (α : Type u) [SemigroupWithZero α] : SemigroupWithZero αᵃᵒᵖ

Equations

• AddOpposite.instSemigroupWithZero α = let __src := AddOpposite.semigroup α; let __src_1 := AddOpposite.instMulZeroClass α; SemigroupWithZero.mk ⋯ ⋯

instance AddOpposite.instMonoidWithZero (α : Type u) [MonoidWithZero α] : MonoidWithZero αᵃᵒᵖ

Equations

• AddOpposite.instMonoidWithZero α = let __src := AddOpposite.monoid α; let __src_1 := AddOpposite.instMulZeroOneClass α; MonoidWithZero.mk ⋯ ⋯

instance AddOpposite.instNonUnitalNonAssocSemiring (α : Type u) [NonUnitalNonAssocSemiring α] : NonUnitalNonAssocSemiring αᵃᵒᵖ

Equations

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

instance AddOpposite.instNonUnitalSemiring (α : Type u) [NonUnitalSemiring α] : NonUnitalSemiring αᵃᵒᵖ

Equations

• AddOpposite.instNonUnitalSemiring α = let __src := AddOpposite.instSemigroupWithZero α; let __src_1 := AddOpposite.instNonUnitalNonAssocSemiring α; NonUnitalSemiring.mk ⋯

instance AddOpposite.instNonAssocSemiring (α : Type u) [NonAssocSemiring α] : NonAssocSemiring αᵃᵒᵖ

Equations

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

instance AddOpposite.instSemiring (α : Type u) [Semiring α] : Semiring αᵃᵒᵖ

Equations

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

instance AddOpposite.instNonUnitalCommSemiring (α : Type u) [NonUnitalCommSemiring α] : NonUnitalCommSemiring αᵃᵒᵖ

Equations

• AddOpposite.instNonUnitalCommSemiring α = let __src := AddOpposite.instNonUnitalSemiring α; let __src_1 := AddOpposite.commSemigroup α; NonUnitalCommSemiring.mk ⋯

instance AddOpposite.instCommSemiring (α : Type u) [CommSemiring α] : CommSemiring αᵃᵒᵖ

Equations

• AddOpposite.instCommSemiring α = let __src := AddOpposite.instSemiring α; let __src_1 := AddOpposite.commSemigroup α; CommSemiring.mk ⋯

instance AddOpposite.instNonUnitalNonAssocRing (α : Type u) [NonUnitalNonAssocRing α] : NonUnitalNonAssocRing αᵃᵒᵖ

Equations

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

instance AddOpposite.instNonUnitalRing (α : Type u) [NonUnitalRing α] : NonUnitalRing αᵃᵒᵖ

Equations

• AddOpposite.instNonUnitalRing α = let __src := AddOpposite.addCommGroup α; let __src_1 := AddOpposite.instSemigroupWithZero α; let __src_2 := AddOpposite.instDistrib α; NonUnitalRing.mk ⋯

instance AddOpposite.instNonAssocRing (α : Type u) [NonAssocRing α] : NonAssocRing αᵃᵒᵖ

Equations

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

instance AddOpposite.instRing (α : Type u) [Ring α] : Ring αᵃᵒᵖ

Equations

• AddOpposite.instRing α = let __src := AddOpposite.instNonAssocRing α; let __src_1 := AddOpposite.instSemiring α; Ring.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance AddOpposite.instNonUnitalCommRing (α : Type u) [NonUnitalCommRing α] : NonUnitalCommRing αᵃᵒᵖ

Equations

• AddOpposite.instNonUnitalCommRing α = let __src := AddOpposite.instNonUnitalRing α; let __src_1 := AddOpposite.instNonUnitalCommSemiring α; NonUnitalCommRing.mk ⋯

instance AddOpposite.instCommRing (α : Type u) [CommRing α] : CommRing αᵃᵒᵖ

Equations

• AddOpposite.instCommRing α = let __src := AddOpposite.instRing α; let __src_1 := AddOpposite.instCommSemiring α; CommRing.mk ⋯

instance AddOpposite.instNoZeroDivisors (α : Type u) [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵃᵒᵖ

Equations

• ⋯ = ⋯

instance AddOpposite.instIsDomain (α : Type u) [Ring α] [IsDomain α] : IsDomain αᵃᵒᵖ

Equations

• ⋯ = ⋯

instance AddOpposite.instGroupWithZero (α : Type u) [GroupWithZero α] : GroupWithZero αᵃᵒᵖ

Equations

• AddOpposite.instGroupWithZero α = let __src := AddOpposite.instMonoidWithZero α; let __src_1 := AddOpposite.divInvMonoid α; let __src_2 := ⋯; GroupWithZero.mk ⋯ DivInvMonoid.zpow ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem NonUnitalRingHom.toOpposite_apply {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : ⇑(NonUnitalRingHom.toOpposite f hf) = MulOpposite.op ∘ ⇑f

def NonUnitalRingHom.toOpposite {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : R →ₙ+* Sᵐᵒᵖ

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

Equations

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

@[simp]

theorem NonUnitalRingHom.fromOpposite_apply {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : ⇑(NonUnitalRingHom.fromOpposite f hf) = ⇑f ∘ MulOpposite.unop

def NonUnitalRingHom.fromOpposite {R : Type u_1} {S : Type u_2} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : Rᵐᵒᵖ →ₙ+* S

A non-unital ring homomorphism f : R →ₙ* S such that f x commutes with f y for all x, y defines a non-unital ring homomorphism from Rᵐᵒᵖ.

Equations

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

@[simp]

theorem NonUnitalRingHom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) : ∀ (a : α), (NonUnitalRingHom.op.symm f) a = (AddMonoidHom.mulUnop (NonUnitalRingHom.toAddMonoidHom f)).toFun a

@[simp]

theorem NonUnitalRingHom.op_apply_apply {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) : ∀ (a : αᵐᵒᵖ), (NonUnitalRingHom.op f) a = (AddMonoidHom.mulOp (NonUnitalRingHom.toAddMonoidHom f)).toFun a

def NonUnitalRingHom.op {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : (α →ₙ+* β) ≃ (αᵐᵒᵖ →ₙ+* βᵐᵒᵖ)

A non-unital ring hom α →ₙ+* β can equivalently be viewed as a non-unital ring hom αᵐᵒᵖ →+* βᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations

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

def NonUnitalRingHom.unop {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] : (αᵐᵒᵖ →ₙ+* βᵐᵒᵖ) ≃ (α →ₙ+* β)

The 'unopposite' of a non-unital ring hom αᵐᵒᵖ →ₙ+* βᵐᵒᵖ. Inverse to NonUnitalRingHom.op.

Equations

• NonUnitalRingHom.unop = NonUnitalRingHom.op.symm

@[simp]

theorem RingHom.toOpposite_apply {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : ⇑(RingHom.toOpposite f hf) = MulOpposite.op ∘ ⇑f

def RingHom.toOpposite {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

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

@[simp]

theorem RingHom.fromOpposite_apply {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) (hf : ∀ (x y : R), Commute (f x) (f y)) : ⇑(RingHom.fromOpposite f hf) = ⇑f ∘ MulOpposite.unop

def RingHom.fromOpposite {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 from Rᵐᵒᵖ.

Equations

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

@[simp]

theorem RingHom.op_apply_apply {α : Type u_1} {β : Type u_2} [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) : ∀ (a : αᵐᵒᵖ), (RingHom.op f) a = MulOpposite.op (f (MulOpposite.unop a))

@[simp]

theorem RingHom.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [NonAssocSemiring α] [NonAssocSemiring β] (f : αᵐᵒᵖ →+* βᵐᵒᵖ) : ∀ (a : α), (RingHom.op.symm f) a = MulOpposite.unop (f (MulOpposite.op a))

def RingHom.op {α : Type u_1} {β : Type u_2} [NonAssocSemiring α] [NonAssocSemiring β] : (α →+* β) ≃ (αᵐᵒᵖ →+* βᵐᵒᵖ)

A ring hom α →+* β can equivalently be viewed as a ring hom αᵐᵒᵖ →+* βᵐᵒᵖ. This is the action of the (fully faithful) ᵐᵒᵖ-functor on morphisms.

Equations

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

def RingHom.unop {α : Type u_1} {β : Type u_2} [NonAssocSemiring α] [NonAssocSemiring β] : (αᵐᵒᵖ →+* βᵐᵒᵖ) ≃ (α →+* β)

The 'unopposite' of a ring hom αᵐᵒᵖ →+* βᵐᵒᵖ. Inverse to RingHom.op.

Equations

• RingHom.unop = RingHom.op.symm