Mathlib.Algebra.GroupWithZero.Opposite

MulOpposite.instMulZeroClass instance

[MulZeroClass α] : MulZeroClass αᵐᵒᵖ

Full source

instance instMulZeroClass [MulZeroClass α] : MulZeroClass αᵐᵒᵖ where
  zero_mul _ := unop_injective <| mul_zero _
  mul_zero _ := unop_injective <| zero_mul _

Multiplicative Zero Class Structure on the Multiplicative Opposite

Informal description

For any type $\alpha$ with a multiplication operation and a zero element that satisfy the multiplicative zero class axioms (i.e., $0 \cdot x = 0$ and $x \cdot 0 = 0$ for all $x \in \alpha$), the multiplicative opposite $\alpha^\text{op}$ also forms a multiplicative zero class with the same properties.

MulOpposite.instMulZeroOneClass instance

[MulZeroOneClass α] : MulZeroOneClass αᵐᵒᵖ

Full source

instance instMulZeroOneClass [MulZeroOneClass α] : MulZeroOneClass αᵐᵒᵖ where
  __ := instMulOneClass
  __ := instMulZeroClass

Multiplicative Opposite Preserves MulZeroOneClass Structure

Informal description

For any type $\alpha$ equipped with a multiplication operation, a zero element, and a multiplicative identity (i.e., a `MulZeroOneClass` structure), the multiplicative opposite $\alpha^\text{op}$ also forms a `MulZeroOneClass` structure. This means that $\alpha^\text{op}$ inherits the multiplication operation (with reversed order), the zero element, and the multiplicative identity from $\alpha$.

MulOpposite.instSemigroupWithZero instance

[SemigroupWithZero α] : SemigroupWithZero αᵐᵒᵖ

Full source

instance instSemigroupWithZero [SemigroupWithZero α] : SemigroupWithZero αᵐᵒᵖ where
  __ := instSemigroup
  __ := instMulZeroClass

Semigroup with Zero Structure on the Multiplicative Opposite

Informal description

For any semigroup with zero $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also a semigroup with zero, where the multiplication is defined by $\text{op}(x) \cdot \text{op}(y) = \text{op}(y \cdot x)$ for all $x, y \in \alpha$ and the zero element is preserved.

MulOpposite.instMonoidWithZero instance

[MonoidWithZero α] : MonoidWithZero αᵐᵒᵖ

Full source

instance instMonoidWithZero [MonoidWithZero α] : MonoidWithZero αᵐᵒᵖ where
  __ := instMonoid
  __ := instMulZeroOneClass

Monoid with Zero Structure on the Multiplicative Opposite

Informal description

For any monoid with zero $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also a monoid with zero. The multiplication in $\alpha^\text{op}$ is defined by $\text{op}(x) \cdot \text{op}(y) = \text{op}(y \cdot x)$ for all $x, y \in \alpha$, and both the zero element and the multiplicative identity are preserved.

MulOpposite.instGroupWithZero instance

[GroupWithZero α] : GroupWithZero αᵐᵒᵖ

Full source

instance instGroupWithZero [GroupWithZero α] : GroupWithZero αᵐᵒᵖ where
  __ := instMonoidWithZero
  __ := instNontrivial
  __ := instDivInvMonoid
  mul_inv_cancel _ hx := unop_injective <| inv_mul_cancel₀ <| unop_injective.ne hx
  inv_zero := unop_injective inv_zero

Group with Zero Structure on the Multiplicative Opposite

Informal description

For any group with zero $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also a group with zero. The multiplication in $\alpha^\text{op}$ is defined by $\text{op}(x) \cdot \text{op}(y) = \text{op}(y \cdot x)$ for all $x, y \in \alpha$, and the zero element, multiplicative identity, and inverses are preserved.

MulOpposite.instNoZeroDivisors instance

[Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵐᵒᵖ

Full source

instance instNoZeroDivisors [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵐᵒᵖ where
  eq_zero_or_eq_zero_of_mul_eq_zero (H : op (_ * _) = op (0 : α)) :=
      Or.casesOn (eq_zero_or_eq_zero_of_mul_eq_zero <| op_injective H)
        (fun hy => Or.inr <| unop_injective <| hy) fun hx => Or.inl <| unop_injective <| hx

No Zero Divisors in the Multiplicative Opposite

Informal description

For any type $\alpha$ equipped with a zero element and a multiplication operation that has no zero divisors, the multiplicative opposite $\alpha^\text{op}$ also has no zero divisors. That is, if $x \cdot y = 0$ implies $x = 0$ or $y = 0$ in $\alpha$, then the same property holds in $\alpha^\text{op}$ with the reversed multiplication.

AddOpposite.instMulZeroClass instance

[MulZeroClass α] : MulZeroClass αᵃᵒᵖ

Full source

instance instMulZeroClass [MulZeroClass α] : MulZeroClass αᵃᵒᵖ where
  zero_mul _ := unop_injective <| zero_mul _
  mul_zero _ := unop_injective <| mul_zero _

`MulZeroClass` Structure on the Additive Opposite

Informal description

For any type $\alpha$ equipped with a multiplication operation and a zero element satisfying the `MulZeroClass` axioms, the additive opposite $\alpha^{\text{aop}}$ also forms a `MulZeroClass`. This means that the multiplication and zero on $\alpha^{\text{aop}}$ inherit the properties from $\alpha$, where the product of any element with zero is zero, and the product operation is compatible with the additive opposite structure.

AddOpposite.instMulZeroOneClass instance

[MulZeroOneClass α] : MulZeroOneClass αᵃᵒᵖ

Full source

instance instMulZeroOneClass [MulZeroOneClass α] : MulZeroOneClass αᵃᵒᵖ where
  __ := instMulOneClass
  __ := instMulZeroClass

`MulZeroOneClass` Structure on the Additive Opposite

Informal description

For any type $\alpha$ with a multiplication operation, a zero element, and a multiplicative identity satisfying the `MulZeroOneClass` axioms, the additive opposite $\alpha^{\text{aop}}$ also forms a `MulZeroOneClass`. This means that the multiplication, zero, and identity on $\alpha^{\text{aop}}$ inherit the properties from $\alpha$, where the product of any element with zero is zero, and the multiplicative identity property is preserved under the additive opposite structure.

AddOpposite.instSemigroupWithZero instance

[SemigroupWithZero α] : SemigroupWithZero αᵃᵒᵖ

Full source

instance instSemigroupWithZero [SemigroupWithZero α] : SemigroupWithZero αᵃᵒᵖ where
  __ := instSemigroup
  __ := instMulZeroClass

Semigroup with Zero Structure on Additive Opposite

Informal description

For any semigroup with zero $\alpha$, the additive opposite $\alpha^{\text{aop}}$ also forms a semigroup with zero. The multiplication operation on $\alpha^{\text{aop}}$ is defined by $(x \cdot y)^{\text{aop}} = y^{\text{aop}} \cdot x^{\text{aop}}$, and the zero element is preserved.

AddOpposite.instMonoidWithZero instance

[MonoidWithZero α] : MonoidWithZero αᵃᵒᵖ

Full source

instance instMonoidWithZero [MonoidWithZero α] : MonoidWithZero αᵃᵒᵖ where
  __ := instMonoid
  __ := instMulZeroOneClass

Monoid with Zero Structure on Additive Opposite

Informal description

For any monoid with zero $\alpha$, the additive opposite $\alpha^{\text{aop}}$ is also a monoid with zero.

AddOpposite.instNoZeroDivisors instance

[Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵃᵒᵖ

Full source

instance instNoZeroDivisors [Zero α] [Mul α] [NoZeroDivisors α] : NoZeroDivisors αᵃᵒᵖ where
  eq_zero_or_eq_zero_of_mul_eq_zero (H : op (_ * _) = op (0 : α)) :=
    Or.imp (fun hx => unop_injective hx) (fun hy => unop_injective hy)
    (@eq_zero_or_eq_zero_of_mul_eq_zero α _ _ _ _ _ <| op_injective H)

No Zero Divisors in the Additive Opposite Structure

Informal description

For any type $\alpha$ with a zero element and a multiplication operation that has no zero divisors, the additive opposite $\alpha^{\text{aop}}$ also has no zero divisors.

AddOpposite.instGroupWithZero instance

[GroupWithZero α] : GroupWithZero αᵃᵒᵖ

Full source

instance instGroupWithZero [GroupWithZero α] : GroupWithZero αᵃᵒᵖ where
  __ := instMonoidWithZero
  __ := instNontrivial
  __ := instDivInvMonoid
  mul_inv_cancel _ hx := unop_injective <| mul_inv_cancel₀ <| unop_injective.ne hx
  inv_zero := unop_injective inv_zero

Group with Zero Structure on Additive Opposite

Informal description

For any group with zero $\alpha$, the additive opposite $\alpha^{\text{aop}}$ is also a group with zero.