Mathlib.Algebra.Group.Opposite

MulOpposite.instNatCast instance

[NatCast α] : NatCast αᵐᵒᵖ

Full source

@[to_additive] instance instNatCast [NatCast α] : NatCast αᵐᵒᵖ where natCast n := op n

Natural Number Casting on Multiplicative Opposites

Informal description

For any type $\alpha$ with a natural number casting operation, the multiplicative opposite $\alpha^\text{op}$ also inherits a natural number casting operation.

MulOpposite.instIntCast instance

[IntCast α] : IntCast αᵐᵒᵖ

Full source

@[to_additive] instance instIntCast [IntCast α] : IntCast αᵐᵒᵖ where intCast n := op n

Integer Casting on Multiplicative Opposites

Informal description

For any type $\alpha$ with an integer casting operation, the multiplicative opposite $\alpha^\text{op}$ also inherits an integer casting operation.

MulOpposite.instAddSemigroup instance

[AddSemigroup α] : AddSemigroup αᵐᵒᵖ

Full source

instance instAddSemigroup [AddSemigroup α] : AddSemigroup αᵐᵒᵖ :=
  unop_injective.addSemigroup _ fun _ _ => rfl

Additive Semigroup Structure on Multiplicative Opposite

Informal description

For any additive semigroup $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also an additive semigroup, where the addition is defined by $\text{op}(x) + \text{op}(y) = \text{op}(x + y)$ for all $x, y \in \alpha$.

MulOpposite.instAddLeftCancelSemigroup instance

[AddLeftCancelSemigroup α] : AddLeftCancelSemigroup αᵐᵒᵖ

Full source

instance instAddLeftCancelSemigroup [AddLeftCancelSemigroup α] : AddLeftCancelSemigroup αᵐᵒᵖ :=
  unop_injective.addLeftCancelSemigroup _ fun _ _ => rfl

Additive Left-Cancelative Semigroup Structure on Multiplicative Opposite

Informal description

For any type $\alpha$ that is an additive left-cancelative semigroup, the multiplicative opposite $\alpha^\text{op}$ is also an additive left-cancelative semigroup. Here, the addition in $\alpha^\text{op}$ is defined by $\text{op}(x) + \text{op}(y) = \text{op}(x + y)$ for all $x, y \in \alpha$, and the left-cancellation property is preserved.

MulOpposite.instAddRightCancelSemigroup instance

[AddRightCancelSemigroup α] : AddRightCancelSemigroup αᵐᵒᵖ

Full source

instance instAddRightCancelSemigroup [AddRightCancelSemigroup α] : AddRightCancelSemigroup αᵐᵒᵖ :=
  unop_injective.addRightCancelSemigroup _ fun _ _ => rfl

Add-Right-Cancel Semigroup Structure on the Multiplicative Opposite

Informal description

For any add-right-cancel semigroup $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also an add-right-cancel semigroup, where addition is defined by $\text{op}(x) + \text{op}(y) = \text{op}(x + y)$ for all $x, y \in \alpha$.

MulOpposite.instAddCommSemigroup instance

[AddCommSemigroup α] : AddCommSemigroup αᵐᵒᵖ

Full source

instance instAddCommSemigroup [AddCommSemigroup α] : AddCommSemigroup αᵐᵒᵖ :=
  unop_injective.addCommSemigroup _ fun _ _ => rfl

Commutative Additive Semigroup Structure on Multiplicative Opposite

Informal description

For any commutative additive semigroup $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also a commutative additive semigroup, where addition is defined by $\text{op}(x) + \text{op}(y) = \text{op}(x + y)$ for all $x, y \in \alpha$.

MulOpposite.instAddZeroClass instance

[AddZeroClass α] : AddZeroClass αᵐᵒᵖ

Full source

instance instAddZeroClass [AddZeroClass α] : AddZeroClass αᵐᵒᵖ :=
  unop_injective.addZeroClass _ (by exact rfl) fun _ _ => rfl

Additive Structure on Multiplicative Opposite

Informal description

For any type $\alpha$ equipped with an addition operation and a zero element, the multiplicative opposite $\alpha^\text{op}$ inherits an addition operation and a zero element, where $\text{op}(x) + \text{op}(y) = \text{op}(x + y)$ for all $x, y \in \alpha$ and $\text{op}(0)$ is the zero element in $\alpha^\text{op}$.

MulOpposite.instAddMonoid instance

[AddMonoid α] : AddMonoid αᵐᵒᵖ

Full source

instance instAddMonoid [AddMonoid α] : AddMonoid αᵐᵒᵖ :=
  unop_injective.addMonoid _ (by exact rfl) (fun _ _ => rfl) fun _ _ => rfl

Additive Monoid Structure on the Multiplicative Opposite

Informal description

For any additively written monoid $\alpha$, the multiplicative opposite $\alpha^\text{op}$ inherits an additively written monoid structure, where addition is defined by $\text{op}(x) + \text{op}(y) = \text{op}(x + y)$ for all $x, y \in \alpha$, and the zero element is $\text{op}(0)$.

MulOpposite.instAddCommMonoid instance

[AddCommMonoid α] : AddCommMonoid αᵐᵒᵖ

Full source

instance instAddCommMonoid [AddCommMonoid α] : AddCommMonoid αᵐᵒᵖ :=
  unop_injective.addCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl

Commutative Additive Monoid Structure on the Multiplicative Opposite

Informal description

For any additively written commutative monoid $\alpha$, the multiplicative opposite $\alpha^\text{op}$ inherits an additively written commutative monoid structure, where addition is defined by $\text{op}(x) + \text{op}(y) = \text{op}(x + y)$ for all $x, y \in \alpha$, and the zero element is $\text{op}(0)$.

MulOpposite.instAddMonoidWithOne instance

[AddMonoidWithOne α] : AddMonoidWithOne αᵐᵒᵖ

Full source

instance instAddMonoidWithOne [AddMonoidWithOne α] : AddMonoidWithOne αᵐᵒᵖ where
  toNatCast := instNatCast
  toAddMonoid := instAddMonoid
  toOne := instOne
  natCast_zero := show op ((0 : ℕ) : α) = 0 by rw [Nat.cast_zero, op_zero]
  natCast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op ↑(n : ℕ) + 1 by simp

Additive Monoid with One Structure on Multiplicative Opposites

Informal description

For any additive monoid with one $\alpha$, the multiplicative opposite $\alpha^\text{op}$ inherits an additive monoid with one structure, where the addition and the distinguished element $1$ are defined via the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$.

MulOpposite.instAddCommMonoidWithOne instance

[AddCommMonoidWithOne α] : AddCommMonoidWithOne αᵐᵒᵖ

Full source

instance instAddCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne αᵐᵒᵖ where
  toAddMonoidWithOne := instAddMonoidWithOne
  __ := instAddCommMonoid

Additive Commutative Monoid with One Structure on Multiplicative Opposites

Informal description

For any additive commutative monoid with one $\alpha$, the multiplicative opposite $\alpha^\text{op}$ inherits an additive commutative monoid with one structure, where addition is defined by $\text{op}(x) + \text{op}(y) = \text{op}(x + y)$ for all $x, y \in \alpha$, and the distinguished element $1$ is $\text{op}(1)$.

MulOpposite.instSubNegMonoid instance

[SubNegMonoid α] : SubNegMonoid αᵐᵒᵖ

Full source

instance instSubNegMonoid [SubNegMonoid α] : SubNegMonoid αᵐᵒᵖ :=
  unop_injective.subNegMonoid _ (by exact rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl

Subnegmonoid Structure on the Multiplicative Opposite

Informal description

For any type $\alpha$ equipped with a subtraction and negation operation forming a subnegmonoid, the multiplicative opposite $\alpha^\text{op}$ inherits a subnegmonoid structure where subtraction and negation are defined componentwise via the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$.

MulOpposite.instAddGroup instance

[AddGroup α] : AddGroup αᵐᵒᵖ

Full source

instance instAddGroup [AddGroup α] : AddGroup αᵐᵒᵖ :=
  unop_injective.addGroup _ (by exact rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
  (fun _ _ => rfl) fun _ _ => rfl

Additive Group Structure on the Multiplicative Opposite

Informal description

For any additive group $\alpha$, the multiplicative opposite $\alpha^\text{op}$ inherits an additive group structure, where addition is defined by $\text{op}(x) + \text{op}(y) = \text{op}(x + y)$ for all $x, y \in \alpha$, the zero element is $\text{op}(0)$, and the negation is given by $\text{op}(-x) = -\text{op}(x)$.

MulOpposite.instAddCommGroup instance

[AddCommGroup α] : AddCommGroup αᵐᵒᵖ

Full source

instance instAddCommGroup [AddCommGroup α] : AddCommGroup αᵐᵒᵖ :=
  unop_injective.addCommGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl

Additive Commutative Group Structure on the Multiplicative Opposite

Informal description

For any additive commutative group $\alpha$, the multiplicative opposite $\alpha^\text{op}$ inherits an additive commutative group structure, where addition is defined by $\text{op}(x) + \text{op}(y) = \text{op}(x + y)$ for all $x, y \in \alpha$, and the zero element is $\text{op}(0)$.

MulOpposite.instAddGroupWithOne instance

[AddGroupWithOne α] : AddGroupWithOne αᵐᵒᵖ

Full source

instance instAddGroupWithOne [AddGroupWithOne α] : AddGroupWithOne αᵐᵒᵖ where
  toAddMonoidWithOne := instAddMonoidWithOne
  toIntCast := instIntCast
  __ := instAddGroup
  intCast_ofNat n := show op ((n : ℤ) : α) = op (n : α) by rw [Int.cast_natCast]
  intCast_negSucc n := show op _ = op (-unop (op ((n + 1 : ℕ) : α))) by simp

Additive Group with One Structure on Multiplicative Opposites

Informal description

For any additive group with one $\alpha$, the multiplicative opposite $\alpha^\text{op}$ inherits an additive group with one structure, where the addition, negation, and distinguished element $1$ are defined via the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$.

MulOpposite.instAddCommGroupWithOne instance

[AddCommGroupWithOne α] : AddCommGroupWithOne αᵐᵒᵖ

Full source

instance instAddCommGroupWithOne [AddCommGroupWithOne α] : AddCommGroupWithOne αᵐᵒᵖ where
  toAddCommGroup := instAddCommGroup
  __ := instAddGroupWithOne

Additive Commutative Group with One Structure on Multiplicative Opposites

Informal description

For any additive commutative group with one $\alpha$, the multiplicative opposite $\alpha^\text{op}$ inherits an additive commutative group with one structure, where the addition, negation, and distinguished element $1$ are defined via the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$.

MulOpposite.instIsRightCancelMul instance

[Mul α] [IsLeftCancelMul α] : IsRightCancelMul αᵐᵒᵖ

Full source

@[to_additive]
instance instIsRightCancelMul [Mul α] [IsLeftCancelMul α] : IsRightCancelMul αᵐᵒᵖ where
  mul_right_cancel _ _ _ h := unop_injective <| mul_left_cancel <| op_injective h

Right Cancellative Property of the Multiplicative Opposite from Left Cancellative Multiplication

Informal description

For any type $\alpha$ with a multiplication operation that is left cancellative, the multiplicative opposite $\alpha^\text{op}$ is right cancellative. That is, if for all $x, y, z \in \alpha$ the equality $x \cdot y = x \cdot z$ implies $y = z$, then for all $a, b, c \in \alpha^\text{op}$ the equality $a \cdot b = a \cdot c$ implies $b = c$.

MulOpposite.instIsLeftCancelMul instance

[Mul α] [IsRightCancelMul α] : IsLeftCancelMul αᵐᵒᵖ

Full source

@[to_additive]
instance instIsLeftCancelMul [Mul α] [IsRightCancelMul α] : IsLeftCancelMul αᵐᵒᵖ where
  mul_left_cancel _ _ _ h := unop_injective <| mul_right_cancel <| op_injective h

Left Cancellative Property of the Multiplicative Opposite of a Right Cancellative Semigroup

Informal description

For any type $\alpha$ with a multiplication operation that is right cancellative (i.e., $x \cdot z = y \cdot z$ implies $x = y$ for all $x, y, z \in \alpha$), the multiplicative opposite $\alpha^\text{op}$ is left cancellative (i.e., $z \cdot x = z \cdot y$ implies $x = y$ for all $x, y, z \in \alpha^\text{op}$).

MulOpposite.instSemigroup instance

[Semigroup α] : Semigroup αᵐᵒᵖ

Full source

@[to_additive]
instance instSemigroup [Semigroup α] : Semigroup αᵐᵒᵖ where
  mul_assoc x y z := unop_injective <| Eq.symm <| mul_assoc (unop z) (unop y) (unop x)

Semigroup Structure on the Multiplicative Opposite

Informal description

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

MulOpposite.instLeftCancelSemigroup instance

[RightCancelSemigroup α] : LeftCancelSemigroup αᵐᵒᵖ

Full source

@[to_additive]
instance instLeftCancelSemigroup [RightCancelSemigroup α] : LeftCancelSemigroup αᵐᵒᵖ where
  mul_left_cancel _ _ _ := mul_left_cancel

Left Cancellative Semigroup Structure on the Multiplicative Opposite of a Right Cancellative Semigroup

Informal description

For any right cancellative semigroup $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is a left cancellative semigroup.

MulOpposite.instRightCancelSemigroup instance

[LeftCancelSemigroup α] : RightCancelSemigroup αᵐᵒᵖ

Full source

@[to_additive]
instance instRightCancelSemigroup [LeftCancelSemigroup α] : RightCancelSemigroup αᵐᵒᵖ where
  mul_right_cancel _ _ _ := mul_right_cancel

Right Cancellation in the Multiplicative Opposite of a Left Cancellative Semigroup

Informal description

For any left cancellative semigroup $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is a right cancellative semigroup. Specifically, if $\alpha$ satisfies the left cancellation property (i.e., $a \cdot b = a \cdot c$ implies $b = c$ for all $a, b, c \in \alpha$), then $\alpha^\text{op}$ satisfies the right cancellation property (i.e., $b \cdot a = c \cdot a$ implies $b = c$ for all $a, b, c \in \alpha^\text{op}$).

MulOpposite.instCommSemigroup instance

[CommSemigroup α] : CommSemigroup αᵐᵒᵖ

Full source

@[to_additive]
instance instCommSemigroup [CommSemigroup α] : CommSemigroup αᵐᵒᵖ where
  mul_comm x y := unop_injective <| mul_comm (unop y) (unop x)

Commutative Semigroup Structure on the Multiplicative Opposite

Informal description

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

MulOpposite.instMulOneClass instance

[MulOneClass α] : MulOneClass αᵐᵒᵖ

Full source

@[to_additive]
instance instMulOneClass [MulOneClass α] : MulOneClass αᵐᵒᵖ where
  toMul := instMul
  toOne := instOne
  one_mul _ := unop_injective <| mul_one _
  mul_one _ := unop_injective <| one_mul _

Multiplicative Opposite Preserves MulOneClass Structure

Informal description

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

MulOpposite.instMonoid instance

[Monoid α] : Monoid αᵐᵒᵖ

Full source

@[to_additive]
instance instMonoid [Monoid α] : Monoid αᵐᵒᵖ where
  toSemigroup := instSemigroup
  __ := instMulOneClass
  npow n a := op <| a.unop ^ n
  npow_zero _ := unop_injective <| pow_zero _
  npow_succ _ _ := unop_injective <| pow_succ' _ _

Monoid Structure on the Multiplicative Opposite

Informal description

For any monoid $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also a monoid, 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 identity element is preserved.

MulOpposite.instLeftCancelMonoid instance

[RightCancelMonoid α] : LeftCancelMonoid αᵐᵒᵖ

Full source

@[to_additive]
instance instLeftCancelMonoid [RightCancelMonoid α] : LeftCancelMonoid αᵐᵒᵖ where
  toMonoid := instMonoid
  __ := instLeftCancelSemigroup

Left Cancellative Monoid Structure on the Multiplicative Opposite of a Right Cancellative Monoid

Informal description

For any right cancellative monoid $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is a left cancellative monoid.

MulOpposite.instRightCancelMonoid instance

[LeftCancelMonoid α] : RightCancelMonoid αᵐᵒᵖ

Full source

@[to_additive]
instance instRightCancelMonoid [LeftCancelMonoid α] : RightCancelMonoid αᵐᵒᵖ where
  toMonoid := instMonoid
  __ := instRightCancelSemigroup

Right Cancellative Monoid Structure on the Multiplicative Opposite of a Left Cancellative Monoid

Informal description

For any left cancellative monoid $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is a right cancellative monoid. Specifically, the multiplication in $\alpha^\text{op}$ satisfies the right cancellation property: for all $x, y, z \in \alpha^\text{op}$, if $x \cdot z = y \cdot z$, then $x = y$.

MulOpposite.instCancelMonoid instance

[CancelMonoid α] : CancelMonoid αᵐᵒᵖ

Full source

@[to_additive]
instance instCancelMonoid [CancelMonoid α] : CancelMonoid αᵐᵒᵖ where
  toLeftCancelMonoid := instLeftCancelMonoid
  __ := instRightCancelMonoid

Cancellative Monoid Structure on the Multiplicative Opposite

Informal description

For any cancellative monoid $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also a cancellative monoid.

MulOpposite.instCommMonoid instance

[CommMonoid α] : CommMonoid αᵐᵒᵖ

Full source

@[to_additive]
instance instCommMonoid [CommMonoid α] : CommMonoid αᵐᵒᵖ where
  toMonoid := instMonoid
  __ := instCommSemigroup

Commutative Monoid Structure on the Multiplicative Opposite

Informal description

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

MulOpposite.instCancelCommMonoid instance

[CancelCommMonoid α] : CancelCommMonoid αᵐᵒᵖ

Full source

@[to_additive]
instance instCancelCommMonoid [CancelCommMonoid α] : CancelCommMonoid αᵐᵒᵖ where
  toCommMonoid := instCommMonoid
  __ := instLeftCancelMonoid

Cancellative Commutative Monoid Structure on the Multiplicative Opposite

Informal description

For any cancellative commutative monoid $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also a cancellative commutative monoid.

MulOpposite.instDivInvMonoid instance

[DivInvMonoid α] : DivInvMonoid αᵐᵒᵖ

Full source

@[to_additive AddOpposite.instSubNegMonoid]
instance instDivInvMonoid [DivInvMonoid α] : DivInvMonoid αᵐᵒᵖ where
  toMonoid := instMonoid
  toInv := instInv
  zpow n a := op <| a.unop ^ n
  zpow_zero' _ := unop_injective <| zpow_zero _
  zpow_succ' _ _ := unop_injective <| by
    rw [unop_op, zpow_natCast, pow_succ', unop_mul, unop_op, zpow_natCast]
  zpow_neg' _ _ := unop_injective <| DivInvMonoid.zpow_neg' _ _

Division and Inversion Monoid Structure on the Multiplicative Opposite

Informal description

For any type $\alpha$ equipped with a division and inversion monoid structure, the multiplicative opposite $\alpha^\text{op}$ also inherits a division and inversion monoid structure, where the operations are defined by $\text{op}(x) \cdot \text{op}(y) = \text{op}(y \cdot x)$, $\text{op}(x)^{-1} = \text{op}(x^{-1})$, and $\text{op}(x) / \text{op}(y) = \text{op}(y^{-1} \cdot x)$ for all $x, y \in \alpha$.

MulOpposite.instDivisionMonoid instance

[DivisionMonoid α] : DivisionMonoid αᵐᵒᵖ

Full source

@[to_additive]
instance instDivisionMonoid [DivisionMonoid α] : DivisionMonoid αᵐᵒᵖ where
  toDivInvMonoid := instDivInvMonoid
  __ := instInvolutiveInv
  mul_inv_rev _ _ := unop_injective <| mul_inv_rev _ _
  inv_eq_of_mul _ _ h := unop_injective <| inv_eq_of_mul_eq_one_left <| congr_arg unop h

Division Monoid Structure on the Multiplicative Opposite

Informal description

For any division monoid $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also a division monoid, where the operations are defined by $\text{op}(x) \cdot \text{op}(y) = \text{op}(y \cdot x)$, $\text{op}(x)^{-1} = \text{op}(x^{-1})$, and $\text{op}(x) / \text{op}(y) = \text{op}(y^{-1} \cdot x)$ for all $x, y \in \alpha$.

MulOpposite.instDivisionCommMonoid instance

[DivisionCommMonoid α] : DivisionCommMonoid αᵐᵒᵖ

Full source

@[to_additive AddOpposite.instSubtractionCommMonoid]
instance instDivisionCommMonoid [DivisionCommMonoid α] : DivisionCommMonoid αᵐᵒᵖ where
  toDivisionMonoid := instDivisionMonoid
  __ := instCommSemigroup

Commutative Division Monoid Structure on the Multiplicative Opposite

Informal description

For any commutative division monoid $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also a commutative division monoid, where the operations are defined by $\text{op}(x) \cdot \text{op}(y) = \text{op}(y \cdot x)$, $\text{op}(x)^{-1} = \text{op}(x^{-1})$, and $\text{op}(x) / \text{op}(y) = \text{op}(y^{-1} \cdot x)$ for all $x, y \in \alpha$.

MulOpposite.instGroup instance

[Group α] : Group αᵐᵒᵖ

Full source

@[to_additive]
instance instGroup [Group α] : Group αᵐᵒᵖ where
  toDivInvMonoid := instDivInvMonoid
  inv_mul_cancel _ := unop_injective <| mul_inv_cancel _

Group Structure on the Multiplicative Opposite

Informal description

For any group $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also a group, where the multiplication is defined by $\text{op}(x) \cdot \text{op}(y) = \text{op}(y \cdot x)$ and the inverse satisfies $\text{op}(x)^{-1} = \text{op}(x^{-1})$ for all $x, y \in \alpha$.

MulOpposite.instCommGroup instance

[CommGroup α] : CommGroup αᵐᵒᵖ

Full source

@[to_additive]
instance instCommGroup [CommGroup α] : CommGroup αᵐᵒᵖ where
  toGroup := instGroup
  __ := instCommSemigroup

Commutative Group Structure on the Multiplicative Opposite

Informal description

For any commutative group $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also a commutative group, where the multiplication is defined by $\text{op}(x) \cdot \text{op}(y) = \text{op}(y \cdot x)$ and the inverse satisfies $\text{op}(x)^{-1} = \text{op}(x^{-1})$ for all $x, y \in \alpha$.

MulOpposite.op_pow theorem

(x : α) (n : ℕ) : op (x ^ n) = op x ^ n

Full source

@[simp] lemma op_pow (x : α) (n : ℕ) : op (x ^ n) = op x ^ n := rfl

Power Preservation in Multiplicative Opposite: $\text{op}(x^n) = (\text{op}(x))^n$

Informal description

For any element $x$ in a monoid $\alpha$ and any natural number $n$, the multiplicative opposite of $x^n$ is equal to the $n$-th power of the multiplicative opposite of $x$, i.e., $\text{op}(x^n) = (\text{op}(x))^n$.

MulOpposite.unop_pow theorem

(x : αᵐᵒᵖ) (n : ℕ) : unop (x ^ n) = unop x ^ n

Full source

@[simp] lemma unop_pow (x : αᵐᵒᵖ) (n : ℕ) : unop (x ^ n) = unop x ^ n := rfl

Power Preservation under Projection from Multiplicative Opposite

Informal description

For any element $x$ in the multiplicative opposite $\alpha^\text{op}$ of a monoid $\alpha$ and any natural number $n$, the projection of $x^n$ back to $\alpha$ equals the $n$-th power of the projection of $x$ in $\alpha$, i.e., $\text{unop}(x^n) = (\text{unop}(x))^n$.

MulOpposite.op_zpow theorem

(x : α) (z : ℤ) : op (x ^ z) = op x ^ z

Full source

@[simp] lemma op_zpow (x : α) (z : ℤ) : op (x ^ z) = op x ^ z := rfl

Integer Power Preservation in Multiplicative Opposite: $\text{op}(x^z) = (\text{op}(x))^z$

Informal description

For any element $x$ in a group $\alpha$ and any integer $z$, the multiplicative opposite of $x^z$ is equal to the $z$-th power of the multiplicative opposite of $x$, i.e., $\text{op}(x^z) = (\text{op}(x))^z$.

MulOpposite.unop_zpow theorem

(x : αᵐᵒᵖ) (z : ℤ) : unop (x ^ z) = unop x ^ z

Full source

@[simp] lemma unop_zpow (x : αᵐᵒᵖ) (z : ℤ) : unop (x ^ z) = unop x ^ z := rfl

Integer Power Preservation under Projection from Multiplicative Opposite

Informal description

For any element $x$ in the multiplicative opposite $\alpha^\text{op}$ of a type $\alpha$ equipped with a division and inversion monoid structure, and for any integer $z$, the projection of $x^z$ back to $\alpha$ equals the $z$-th power of the projection of $x$ in $\alpha$, i.e., $\text{unop}(x^z) = (\text{unop}(x))^z$.

MulOpposite.op_natCast theorem

[NatCast α] (n : ℕ) : op (n : α) = n

Full source

@[to_additive (attr := simp, norm_cast)]
theorem op_natCast [NatCast α] (n : ℕ) : op (n : α) = n :=
  rfl

Preservation of Natural Number Cast in Multiplicative Opposite

Informal description

For any type $\alpha$ with a natural number casting operation and for any natural number $n$, the canonical embedding $\text{op}$ into the multiplicative opposite $\alpha^\text{op}$ preserves the natural number cast, i.e., $\text{op}(n) = n$.

MulOpposite.op_ofNat theorem

[NatCast α] (n : ℕ) [n.AtLeastTwo] : op (ofNat(n) : α) = ofNat(n)

Full source

@[to_additive (attr := simp)]
theorem op_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] :
    op (ofNat(n) : α) = ofNat(n) :=
  rfl

Preservation of Numerals ≥ 2 in Multiplicative Opposite

Informal description

For any type $\alpha$ with a natural number casting operation and any natural number $n \geq 2$, the canonical embedding $\text{op}$ into the multiplicative opposite $\alpha^\text{op}$ preserves the numeral interpretation, i.e., $\text{op}(n) = n$.

MulOpposite.op_intCast theorem

[IntCast α] (n : ℤ) : op (n : α) = n

Full source

@[to_additive (attr := simp, norm_cast)]
theorem op_intCast [IntCast α] (n : ℤ) : op (n : α) = n :=
  rfl

Preservation of Integer Cast in Multiplicative Opposite

Informal description

For any type $\alpha$ with an integer casting operation and for any integer $n$, the canonical embedding $\text{op}$ into the multiplicative opposite $\alpha^\text{op}$ preserves the integer cast, i.e., $\text{op}(n) = n$.

MulOpposite.unop_natCast theorem

[NatCast α] (n : ℕ) : unop (n : αᵐᵒᵖ) = n

Full source

@[to_additive (attr := simp, norm_cast)]
theorem unop_natCast [NatCast α] (n : ℕ) : unop (n : αᵐᵒᵖ) = n :=
  rfl

Projection of Natural Numbers in Multiplicative Opposite Equals Original

Informal description

For any type $\alpha$ with a natural number casting operation and any natural number $n$, the canonical projection from the multiplicative opposite $\alpha^\text{op}$ satisfies $\text{unop}(n) = n$, where $n$ is interpreted in $\alpha^\text{op}$ via the natural number casting operation.

MulOpposite.unop_ofNat theorem

[NatCast α] (n : ℕ) [n.AtLeastTwo] : unop (ofNat(n) : αᵐᵒᵖ) = ofNat(n)

Full source

@[to_additive (attr := simp)]
theorem unop_ofNat [NatCast α] (n : ℕ) [n.AtLeastTwo] :
    unop (ofNat(n) : αᵐᵒᵖ) = ofNat(n) :=
  rfl

Projection of Numerals ≥ 2 in Multiplicative Opposite Equals Original

Informal description

For any type $\alpha$ with a natural number casting operation and any natural number $n \geq 2$, the canonical projection from the multiplicative opposite $\alpha^\text{op}$ satisfies $\text{unop}(n) = n$, where $n$ is interpreted in $\alpha^\text{op}$ via the `OfNat` instance.

MulOpposite.unop_intCast theorem

[IntCast α] (n : ℤ) : unop (n : αᵐᵒᵖ) = n

Full source

@[to_additive (attr := simp, norm_cast)]
theorem unop_intCast [IntCast α] (n : ℤ) : unop (n : αᵐᵒᵖ) = n :=
  rfl

Projection of Integers in Multiplicative Opposite Equals Original

Informal description

For any type $\alpha$ with an integer casting operation and any integer $n$, the canonical projection from the multiplicative opposite $\alpha^\text{op}$ satisfies $\text{unop}(n) = n$, where $n$ is interpreted in $\alpha^\text{op}$ via the integer casting operation.

MulOpposite.unop_div theorem

[DivInvMonoid α] (x y : αᵐᵒᵖ) : unop (x / y) = (unop y)⁻¹ * unop x

Full source

@[to_additive (attr := simp)]
theorem unop_div [DivInvMonoid α] (x y : αᵐᵒᵖ) : unop (x / y) = (unop y)⁻¹ * unop x :=
  rfl

Projection of Division in Multiplicative Opposite Equals Inverse Product of Projections

Informal description

For any elements $x, y$ in the multiplicative opposite $\alpha^\text{op}$ of a division and inversion monoid $\alpha$, the projection of their division satisfies $\text{unop}(x / y) = (\text{unop}(y))^{-1} \cdot \text{unop}(x)$.

MulOpposite.op_div theorem

[DivInvMonoid α] (x y : α) : op (x / y) = (op y)⁻¹ * op x

Full source

@[to_additive (attr := simp)]
theorem op_div [DivInvMonoid α] (x y : α) : op (x / y) = (op y)⁻¹ * op x := by simp [div_eq_mul_inv]

Multiplicative Opposite of Division Equals Inverse Product of Opposites

Informal description

For any elements $x, y$ in a type $\alpha$ equipped with division and inversion operations, the multiplicative opposite of the division $x / y$ is equal to the product of the inverse of the opposite of $y$ and the opposite of $x$, i.e., $\text{op}(x / y) = (\text{op}(y))^{-1} \cdot \text{op}(x)$.

MulOpposite.semiconjBy_op theorem

[Mul α] {a x y : α} : SemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y

Full source

@[to_additive (attr := simp)]
theorem semiconjBy_op [Mul α] {a x y : α} : SemiconjBySemiconjBy (op a) (op y) (op x) ↔ SemiconjBy a x y := by
  simp only [SemiconjBy, ← op_mul, op_inj, eq_comm]

Semiconjugacy Relation in Multiplicative Opposite

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $a, x, y \in \alpha$. The elements $\text{op}(a), \text{op}(y), \text{op}(x)$ in the multiplicative opposite $\alpha^\text{op}$ satisfy the semiconjugacy relation $\text{op}(a) \cdot \text{op}(y) = \text{op}(x) \cdot \text{op}(a)$ if and only if the original elements satisfy $a \cdot x = y \cdot a$ in $\alpha$.

MulOpposite.semiconjBy_unop theorem

[Mul α] {a x y : αᵐᵒᵖ} : SemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y

Full source

@[to_additive (attr := simp, nolint simpComm)]
theorem semiconjBy_unop [Mul α] {a x y : αᵐᵒᵖ} :
    SemiconjBySemiconjBy (unop a) (unop y) (unop x) ↔ SemiconjBy a x y := by
  conv_rhs => rw [← op_unop a, ← op_unop x, ← op_unop y, semiconjBy_op]

Semiconjugacy Relation via Projection from Multiplicative Opposite

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $a, x, y$ be elements of the multiplicative opposite $\alpha^\text{op}$. The elements $\text{unop}(a), \text{unop}(y), \text{unop}(x)$ in $\alpha$ satisfy the semiconjugacy relation $\text{unop}(a) \cdot \text{unop}(x) = \text{unop}(y) \cdot \text{unop}(a)$ if and only if the original elements $a, x, y$ satisfy the semiconjugacy relation $a \cdot x = y \cdot a$ in $\alpha^\text{op}$.

SemiconjBy.op theorem

[Mul α] {a x y : α} (h : SemiconjBy a x y) : SemiconjBy (op a) (op y) (op x)

Full source

@[to_additive]
theorem _root_.SemiconjBy.op [Mul α] {a x y : α} (h : SemiconjBy a x y) :
    SemiconjBy (op a) (op y) (op x) :=
  semiconjBy_op.2 h

Semiconjugacy in the Multiplicative Opposite

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $a, x, y \in \alpha$. If $a$ semiconjugates $x$ to $y$ (i.e., $a \cdot x = y \cdot a$), then in the multiplicative opposite $\alpha^\text{op}$, the element $\text{op}(a)$ semiconjugates $\text{op}(y)$ to $\text{op}(x)$ (i.e., $\text{op}(a) \cdot \text{op}(y) = \text{op}(x) \cdot \text{op}(a)$).

SemiconjBy.unop theorem

[Mul α] {a x y : αᵐᵒᵖ} (h : SemiconjBy a x y) : SemiconjBy (unop a) (unop y) (unop x)

Full source

@[to_additive]
theorem _root_.SemiconjBy.unop [Mul α] {a x y : αᵐᵒᵖ} (h : SemiconjBy a x y) :
    SemiconjBy (unop a) (unop y) (unop x) :=
  semiconjBy_unop.2 h

Semiconjugacy Relation Preserved Under Projection from Multiplicative Opposite

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $a, x, y$ be elements of the multiplicative opposite $\alpha^\text{op}$. If $a$ semiconjugates $x$ to $y$ in $\alpha^\text{op}$ (i.e., $a \cdot x = y \cdot a$), then the projections $\text{unop}(a), \text{unop}(y), \text{unop}(x)$ in $\alpha$ satisfy the semiconjugacy relation $\text{unop}(a) \cdot \text{unop}(x) = \text{unop}(y) \cdot \text{unop}(a)$.

Commute.op theorem

[Mul α] {x y : α} (h : Commute x y) : Commute (op x) (op y)

Full source

@[to_additive]
theorem _root_.Commute.op [Mul α] {x y : α} (h : Commute x y) : Commute (op x) (op y) :=
  SemiconjBy.op h

Commutation Preserved in Multiplicative Opposite

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $x, y \in \alpha$ be commuting elements (i.e., $x \cdot y = y \cdot x$). Then their images under the canonical embedding into the multiplicative opposite $\alpha^\text{op}$ also commute, i.e., $\text{op}(x) \cdot \text{op}(y) = \text{op}(y) \cdot \text{op}(x)$.

Commute.unop theorem

[Mul α] {x y : αᵐᵒᵖ} (h : Commute x y) : Commute (unop x) (unop y)

Full source

@[to_additive]
nonrec theorem _root_.Commute.unop [Mul α] {x y : αᵐᵒᵖ} (h : Commute x y) :
    Commute (unop x) (unop y) :=
  h.unop

Commutation Preserved Under Projection from Multiplicative Opposite

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $x, y$ be elements of the multiplicative opposite $\alpha^\text{op}$. If $x$ and $y$ commute in $\alpha^\text{op}$ (i.e., $x \cdot y = y \cdot x$), then their projections $\text{unop}(x)$ and $\text{unop}(y)$ in $\alpha$ also commute (i.e., $\text{unop}(x) \cdot \text{unop}(y) = \text{unop}(y) \cdot \text{unop}(x)$).

MulOpposite.commute_op theorem

[Mul α] {x y : α} : Commute (op x) (op y) ↔ Commute x y

Full source

@[to_additive (attr := simp)]
theorem commute_op [Mul α] {x y : α} : CommuteCommute (op x) (op y) ↔ Commute x y :=
  semiconjBy_op

Commutation in Multiplicative Opposite iff Commutation in Original Type

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $x, y \in \alpha$. The elements $\text{op}(x)$ and $\text{op}(y)$ in the multiplicative opposite $\alpha^\text{op}$ commute if and only if $x$ and $y$ commute in $\alpha$, i.e., $\text{op}(x) \cdot \text{op}(y) = \text{op}(y) \cdot \text{op}(x)$ if and only if $x \cdot y = y \cdot x$.

MulOpposite.commute_unop theorem

[Mul α] {x y : αᵐᵒᵖ} : Commute (unop x) (unop y) ↔ Commute x y

Full source

@[to_additive (attr := simp, nolint simpComm)]
theorem commute_unop [Mul α] {x y : αᵐᵒᵖ} : CommuteCommute (unop x) (unop y) ↔ Commute x y :=
  semiconjBy_unop

Commutation in Multiplicative Opposite via Projection to Original Type

Informal description

Let $\alpha$ be a type with a multiplication operation, and let $x, y$ be elements of the multiplicative opposite $\alpha^\text{op}$. The elements $\text{unop}(x)$ and $\text{unop}(y)$ in $\alpha$ commute if and only if $x$ and $y$ commute in $\alpha^\text{op}$, i.e., $\text{unop}(x) \cdot \text{unop}(y) = \text{unop}(y) \cdot \text{unop}(x)$ if and only if $x \cdot y = y \cdot x$ in $\alpha^\text{op}$.

AddOpposite.instSemigroup instance

[Semigroup α] : Semigroup αᵃᵒᵖ

Full source

instance instSemigroup [Semigroup α] : Semigroup αᵃᵒᵖ := unop_injective.semigroup _ fun _ _ ↦ rfl

Semigroup Structure on Additive Opposite

Informal description

For any semigroup $\alpha$, the additive opposite $\alpha^{\text{aop}}$ also forms a semigroup, where the operation is defined by $(x \cdot y)^{\text{aop}} = y^{\text{aop}} \cdot x^{\text{aop}}$.

AddOpposite.instLeftCancelSemigroup instance

[LeftCancelSemigroup α] : LeftCancelSemigroup αᵃᵒᵖ

Full source

instance instLeftCancelSemigroup [LeftCancelSemigroup α] : LeftCancelSemigroup αᵃᵒᵖ :=
  unop_injective.leftCancelSemigroup _ fun _ _ => rfl

Left Cancellative Semigroup Structure on Additive Opposite

Informal description

For any left cancellative semigroup $\alpha$, the additive opposite $\alpha^{\text{aop}}$ is also a left cancellative semigroup.

AddOpposite.instRightCancelSemigroup instance

[RightCancelSemigroup α] : RightCancelSemigroup αᵃᵒᵖ

Full source

instance instRightCancelSemigroup [RightCancelSemigroup α] : RightCancelSemigroup αᵃᵒᵖ :=
  unop_injective.rightCancelSemigroup _ fun _ _ => rfl

Right Cancellative Semigroup Structure on the Additive Opposite

Informal description

For any right cancellative semigroup $\alpha$, the additive opposite $\alpha^{\text{aop}}$ is also a right cancellative semigroup.

AddOpposite.instCommSemigroup instance

[CommSemigroup α] : CommSemigroup αᵃᵒᵖ

Full source

instance instCommSemigroup [CommSemigroup α] : CommSemigroup αᵃᵒᵖ :=
  unop_injective.commSemigroup _ fun _ _ => rfl

Commutative Semigroup Structure on Additive Opposite

Informal description

For any commutative semigroup $\alpha$, the additive opposite $\alpha^{\text{aop}}$ is also a commutative semigroup.

AddOpposite.instMulOneClass instance

[MulOneClass α] : MulOneClass αᵃᵒᵖ

Full source

instance instMulOneClass [MulOneClass α] : MulOneClass αᵃᵒᵖ :=
  unop_injective.mulOneClass _ (by exact rfl) fun _ _ => rfl

Multiplicative Identity Structure on the Additive Opposite

Informal description

For any type $\alpha$ with a multiplication operation and a distinguished element $1$ satisfying the multiplicative identity property, the additive opposite $\alpha^{\text{aop}}$ also forms a `MulOneClass` structure, where the multiplication and identity are inherited from $\alpha$.

AddOpposite.pow instance

{β} [Pow α β] : Pow αᵃᵒᵖ β

Full source

instance pow {β} [Pow α β] : Pow αᵃᵒᵖ β where pow a b := op (unop a ^ b)

Power Operation on Additive Opposite

Informal description

For any type $\alpha$ with a power operation $\alpha^\beta$ and any type $\beta$, the additive opposite $\alpha^{\text{op}}$ inherits a power operation $\alpha^{\text{op}}^\beta$ defined by $(a^{\text{op}})^b = (a^b)^{\text{op}}$.

AddOpposite.op_pow theorem

{β} [Pow α β] (a : α) (b : β) : op (a ^ b) = op a ^ b

Full source

@[simp]
theorem op_pow {β} [Pow α β] (a : α) (b : β) : op (a ^ b) = op a ^ b :=
  rfl

Exponentiation Commutes with Additive Opposite Operation

Informal description

For any type $\alpha$ with a power operation $\alpha^\beta$ and any type $\beta$, the operation of taking the additive opposite commutes with exponentiation. Specifically, for any $a \in \alpha$ and $b \in \beta$, we have $\text{op}(a^b) = (\text{op } a)^b$.

AddOpposite.unop_pow theorem

{β} [Pow α β] (a : αᵃᵒᵖ) (b : β) : unop (a ^ b) = unop a ^ b

Full source

@[simp]
theorem unop_pow {β} [Pow α β] (a : αᵃᵒᵖ) (b : β) : unop (a ^ b) = unop a ^ b :=
  rfl

Power Operation on Additive Opposite Preserves Unopposite

Informal description

For any type $\alpha$ with a power operation $\alpha^\beta$ and any type $\beta$, if $a$ is an element of the additive opposite $\alpha^{\text{op}}$ and $b$ is an element of $\beta$, then the unopposite of $a^b$ equals the unopposite of $a$ raised to the power $b$, i.e., $\text{unop}(a^b) = (\text{unop } a)^b$.

AddOpposite.instMonoid instance

[Monoid α] : Monoid αᵃᵒᵖ

Full source

instance instMonoid [Monoid α] : Monoid αᵃᵒᵖ :=
  unop_injective.monoid _ (by exact rfl) (fun _ _ => rfl) fun _ _ => rfl

Monoid Structure on the Additive Opposite

Informal description

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

AddOpposite.instCommMonoid instance

[CommMonoid α] : CommMonoid αᵃᵒᵖ

Full source

instance instCommMonoid [CommMonoid α] : CommMonoid αᵃᵒᵖ :=
  unop_injective.commMonoid _ (by exact rfl) (fun _ _ => rfl) fun _ _ => rfl

Commutative Monoid Structure on Additive Opposite

Informal description

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

AddOpposite.instDivInvMonoid instance

[DivInvMonoid α] : DivInvMonoid αᵃᵒᵖ

Full source

instance instDivInvMonoid [DivInvMonoid α] : DivInvMonoid αᵃᵒᵖ :=
  unop_injective.divInvMonoid _ (by exact rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl

Division Monoid Structure on the Additive Opposite

Informal description

For any type $\alpha$ that is a division monoid (i.e., a monoid with division and inversion operations), the additive opposite $\alpha^\text{aop}$ is also a division monoid. The division and inversion operations on $\alpha^\text{aop}$ are defined in terms of the corresponding operations on $\alpha$ via the canonical map $\text{op} : \alpha \to \alpha^\text{aop}$.

AddOpposite.instGroup instance

[Group α] : Group αᵃᵒᵖ

Full source

instance instGroup [Group α] : Group αᵃᵒᵖ :=
  unop_injective.group _ (by exact rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl

Group Structure on the Additive Opposite of a Group

Informal description

For any group $\alpha$, the additive opposite $\alpha^{\text{aop}}$ is also a group. The group operations on $\alpha^{\text{aop}}$ are defined in terms of the corresponding operations on $\alpha$, with the order of multiplication reversed.

AddOpposite.instCommGroup instance

[CommGroup α] : CommGroup αᵃᵒᵖ

Full source

instance instCommGroup [CommGroup α] : CommGroup αᵃᵒᵖ :=
  unop_injective.commGroup _ (by exact rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
    (fun _ _ => rfl) fun _ _ => rfl

Additive Opposite of a Commutative Group is a Commutative Group

Informal description

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

AddOpposite.instAddCommMonoidWithOne instance

[AddCommMonoidWithOne α] : AddCommMonoidWithOne αᵃᵒᵖ

Full source

instance instAddCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne αᵃᵒᵖ where
  toNatCast := instNatCast
  toOne := instOne
  __ := instAddCommMonoid
  natCast_zero := show op ((0 : ℕ) : α) = 0 by rw [Nat.cast_zero, op_zero]
  natCast_succ := show ∀ n, op ((n + 1 : ℕ) : α) = op ↑(n : ℕ) + 1 by simp [add_comm]

Additive Opposite of an Additive Commutative Monoid with One

Informal description

For any additive commutative monoid with one $\alpha$, the additive opposite $\alpha^{\text{aop}}$ is also an additive commutative monoid with one.

AddOpposite.instAddCommGroupWithOne instance

[AddCommGroupWithOne α] : AddCommGroupWithOne αᵃᵒᵖ

Full source

instance instAddCommGroupWithOne [AddCommGroupWithOne α] : AddCommGroupWithOne αᵃᵒᵖ where
  toIntCast := instIntCast
  toAddCommGroup := instAddCommGroup
  __ := instAddCommMonoidWithOne
  intCast_ofNat _ := congr_arg op <| Int.cast_natCast _
  intCast_negSucc _ := congr_arg op <| Int.cast_negSucc _

Additive Opposite of an Additive Commutative Group with One

Informal description

For any additive commutative group with one $\alpha$, the additive opposite $\alpha^{\text{aop}}$ is also an additive commutative group with one.