Ring structures on the multiplicative opposite #
Equations
- MulOpposite.instDistrib = Distrib.mk ⋯ ⋯
Equations
- MulOpposite.instMulZeroClass = MulZeroClass.mk ⋯ ⋯
Equations
- MulOpposite.instMulZeroOneClass = let __spread.0 := MulOpposite.instMulOneClass; let __spread.1 := MulOpposite.instMulZeroClass; MulZeroOneClass.mk ⋯ ⋯
Equations
- MulOpposite.instSemigroupWithZero = let __spread.0 := MulOpposite.instSemigroup; let __spread.1 := MulOpposite.instMulZeroClass; SemigroupWithZero.mk ⋯ ⋯
Equations
- MulOpposite.instMonoidWithZero = let __spread.0 := MulOpposite.instMonoid; let __spread.1 := MulOpposite.instMulZeroOneClass; MonoidWithZero.mk ⋯ ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- MulOpposite.instNonUnitalSemiring = let __spread.0 := MulOpposite.instNonUnitalNonAssocSemiring; let __spread.1 := MulOpposite.instSemigroupWithZero; NonUnitalSemiring.mk ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- MulOpposite.instNonUnitalCommSemiring = let __spread.0 := MulOpposite.instNonUnitalSemiring; let __spread.1 := MulOpposite.instCommSemigroup; NonUnitalCommSemiring.mk ⋯
Equations
- MulOpposite.instCommSemiring = let __spread.0 := MulOpposite.instSemiring; let __spread.1 := MulOpposite.instCommMonoid; CommSemiring.mk ⋯
Equations
- MulOpposite.instNonUnitalNonAssocRing = let __spread.0 := MulOpposite.instAddCommGroup; let __spread.1 := MulOpposite.instNonUnitalNonAssocSemiring; NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯
Equations
- MulOpposite.instNonUnitalRing = let __spread.0 := MulOpposite.instNonUnitalNonAssocRing; let __spread.1 := MulOpposite.instNonUnitalSemiring; NonUnitalRing.mk ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- MulOpposite.instNonUnitalCommRing = let __spread.0 := MulOpposite.instNonUnitalRing; let __spread.1 := MulOpposite.instNonUnitalCommSemiring; NonUnitalCommRing.mk ⋯
Equations
- MulOpposite.instCommRing = let __spread.0 := MulOpposite.instRing; let __spread.1 := MulOpposite.instCommMonoid; CommRing.mk ⋯
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddOpposite.instDistrib = Distrib.mk ⋯ ⋯
Equations
- AddOpposite.instMulZeroClass = MulZeroClass.mk ⋯ ⋯
Equations
- AddOpposite.instMulZeroOneClass = let __spread.0 := AddOpposite.instMulOneClass; let __spread.1 := AddOpposite.instMulZeroClass; MulZeroOneClass.mk ⋯ ⋯
Equations
- AddOpposite.instSemigroupWithZero = let __spread.0 := AddOpposite.instSemigroup; let __spread.1 := AddOpposite.instMulZeroClass; SemigroupWithZero.mk ⋯ ⋯
Equations
- AddOpposite.instMonoidWithZero = let __spread.0 := AddOpposite.instMonoid; let __spread.1 := AddOpposite.instMulZeroOneClass; MonoidWithZero.mk ⋯ ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddOpposite.instNonUnitalSemiring = let __spread.0 := AddOpposite.instNonUnitalNonAssocSemiring; let __spread.1 := AddOpposite.instSemigroupWithZero; NonUnitalSemiring.mk ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddOpposite.instNonUnitalCommSemiring = let __spread.0 := AddOpposite.instNonUnitalSemiring; let __spread.1 := AddOpposite.instCommSemigroup; NonUnitalCommSemiring.mk ⋯
Equations
- AddOpposite.instCommSemiring = let __spread.0 := AddOpposite.instSemiring; let __spread.1 := AddOpposite.instCommMonoid; CommSemiring.mk ⋯
Equations
- AddOpposite.instNonUnitalNonAssocRing = let __spread.0 := AddOpposite.instAddCommGroup; let __spread.1 := AddOpposite.instNonUnitalNonAssocSemiring; NonUnitalNonAssocRing.mk ⋯ ⋯ ⋯ ⋯
Equations
- AddOpposite.instNonUnitalRing = let __spread.0 := AddOpposite.instNonUnitalNonAssocRing; let __spread.1 := AddOpposite.instNonUnitalSemiring; NonUnitalRing.mk ⋯
Equations
- One or more equations did not get rendered due to their size.
Equations
- AddOpposite.instNonUnitalCommRing = let __spread.0 := AddOpposite.instNonUnitalRing; let __spread.1 := AddOpposite.instNonUnitalCommSemiring; NonUnitalCommRing.mk ⋯
Equations
- AddOpposite.instCommRing = let __spread.0 := AddOpposite.instRing; let __spread.1 := AddOpposite.instCommMonoid; CommRing.mk ⋯
Equations
- ⋯ = ⋯
Equations
- One or more equations did not get rendered due to their size.
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
Instances For
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.
Instances For
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.
Instances For
The 'unopposite' of a non-unital ring hom αᵐᵒᵖ →ₙ+* βᵐᵒᵖ
. Inverse to
NonUnitalRingHom.op
.
Equations
- NonUnitalRingHom.unop = NonUnitalRingHom.op.symm
Instances For
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.
Instances For
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.
Instances For
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.
Instances For
The 'unopposite' of a ring hom αᵐᵒᵖ →+* βᵐᵒᵖ
. Inverse to RingHom.op
.
Equations
- RingHom.unop = RingHom.op.symm