Mathlib.Algebra.Opposites

PreOpposite structure

(α : Type*)

Full source

/-- Auxiliary type to implement `MulOpposite` and `AddOpposite`.

It turns out to be convenient to have `MulOpposite α = AddOpposite α` true by definition, in the
same way that it is convenient to have `Additive α = α`; this means that we also get the defeq
`AddOpposite (Additive α) = MulOpposite α`, which is convenient when working with quotients.

This is a compromise between making `MulOpposite α = AddOpposite α = α` (what we had in Lean 3) and
having no defeqs within those three types (which we had as of https://github.com/leanprover-community/mathlib4/pull/1036). -/
structure PreOpposite (α : Type*) : Type _ where
  /-- The element of `PreOpposite α` that represents `x : α`. -/ op' ::
  /-- The element of `α` represented by `x : PreOpposite α`. -/ unop' : α

Pre-opposite type

Informal description

The auxiliary type `PreOpposite α` is used to implement both `MulOpposite α` (the multiplicative opposite) and `AddOpposite α` (the additive opposite) in a way that ensures definitional equality `MulOpposite α = AddOpposite α`. This setup is convenient for working with quotients and maintains consistency with the desired properties of these opposite structures.

MulOpposite definition

(α : Type*) : Type _

Full source

/-- Multiplicative opposite of a type. This type inherits all additive structures on `α` and
reverses left and right in multiplication. -/
@[to_additive
      "Additive opposite of a type. This type inherits all multiplicative structures on `α` and
      reverses left and right in addition."]
def MulOpposite (α : Type*) : Type _ := PreOpposite α

Multiplicative opposite of a type

Informal description

The multiplicative opposite of a type $\alpha$, denoted $\alpha^\text{op}$, is a structure that inherits all additive algebraic structures from $\alpha$ and reverses the order of multiplication. Specifically, for any $x, y \in \alpha$, the multiplication in $\alpha^\text{op}$ satisfies $\text{op}(x * y) = \text{op}(y) * \text{op}(x)$, where $\text{op} : \alpha \to \alpha^\text{op}$ is the canonical embedding.

term_ᵐᵒᵖ definition

: Lean.TrailingParserDescr✝

Full source

/-- Multiplicative opposite of a type. -/
postfix:max "ᵐᵒᵖ" => MulOpposite

Multiplicative opposite of a type

Informal description

The notation `αᵐᵒᵖ` denotes the multiplicative opposite of a type `α`, which is a structure with one field that reverses the order of multiplication. Specifically, for `x, y : α`, the multiplication in `αᵐᵒᵖ` satisfies `op (x * y) = op y * op x`, where `op` is the canonical map from `α` to `αᵐᵒᵖ`.

term_ᵃᵒᵖ definition

: Lean.TrailingParserDescr✝

Full source

/-- Additive opposite of a type. -/
postfix:max "ᵃᵒᵖ" => AddOpposite

Additive opposite of a type

Informal description

The notation `αᵃᵒᵖ` denotes the additive opposite of a type `α`, which is a structure with one field that reverses the order of summands in additive structures. Specifically, for any `x, y : α`, the canonical map `op : α → αᵃᵒᵖ` satisfies `op (x + y) = op y + op x`.

MulOpposite.op definition

: α → αᵐᵒᵖ

Full source

/-- The element of `MulOpposite α` that represents `x : α`. -/
@[to_additive "The element of `αᵃᵒᵖ` that represents `x : α`."]
def op : α → αᵐᵒᵖ :=
  PreOpposite.op'

Canonical embedding into multiplicative opposite

Informal description

The function maps an element $ x $ of type $ \alpha $ to its multiplicative opposite $ \text{op}(x) $ in $ \alpha^\text{op} $, where multiplication is reversed.

MulOpposite.unop definition

: αᵐᵒᵖ → α

Full source

/-- The element of `α` represented by `x : αᵐᵒᵖ`. -/
@[to_additive (attr := pp_nodot) "The element of `α` represented by `x : αᵃᵒᵖ`."]
def unop : αᵐᵒᵖ → α :=
  PreOpposite.unop'

Canonical projection from multiplicative opposite to original type

Informal description

The function maps an element $ x $ of the multiplicative opposite $ \alpha^\text{op} $ back to the original element in $ \alpha $.

MulOpposite.unop_op theorem

(x : α) : unop (op x) = x

Full source

@[to_additive (attr := simp)]
theorem unop_op (x : α) : unop (op x) = x := rfl

Projection of Embedding into Multiplicative Opposite Yields Original Element

Informal description

For any element $x$ of type $\alpha$, the canonical projection from the multiplicative opposite $\alpha^\text{op}$ back to $\alpha$ satisfies $\text{unop}(\text{op}(x)) = x$.

MulOpposite.op_unop theorem

(x : αᵐᵒᵖ) : op (unop x) = x

Full source

@[to_additive (attr := simp)]
theorem op_unop (x : αᵐᵒᵖ) : op (unop x) = x :=
  rfl

Embedding of Projection from Multiplicative Opposite Yields Original Element

Informal description

For any element $x$ in the multiplicative opposite $\alpha^\text{op}$, the canonical embedding $\text{op}$ applied to the projection $\text{unop}(x)$ yields $x$ itself, i.e., $\text{op}(\text{unop}(x)) = x$.

MulOpposite.op_comp_unop theorem

: (op : α → αᵐᵒᵖ) ∘ unop = id

Full source

@[to_additive (attr := simp)]
theorem op_comp_unop : (op : α → αᵐᵒᵖ) ∘ unop = id :=
  rfl

Identity Property of Multiplicative Opposite's Canonical Maps

Informal description

The composition of the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$ with the canonical projection $\text{unop} : \alpha^\text{op} \to \alpha$ is equal to the identity function on $\alpha^\text{op}$, i.e., $\text{op} \circ \text{unop} = \text{id}_{\alpha^\text{op}}$.

MulOpposite.unop_comp_op theorem

: (unop : αᵐᵒᵖ → α) ∘ op = id

Full source

@[to_additive (attr := simp)]
theorem unop_comp_op : (unop : αᵐᵒᵖ → α) ∘ op = id :=
  rfl

Identity Property of Multiplicative Opposite's Canonical Maps

Informal description

The composition of the canonical projection $\text{unop} : \alpha^\text{op} \to \alpha$ with the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$ is equal to the identity function on $\alpha$, i.e., $\text{unop} \circ \text{op} = \text{id}_\alpha$.

MulOpposite.rec' definition

{F : αᵐᵒᵖ → Sort*} (h : ∀ X, F (op X)) : ∀ X, F X

Full source

/-- A recursor for `MulOpposite`. Use as `induction x`. -/
@[to_additive (attr := simp, elab_as_elim, induction_eliminator, cases_eliminator)
  "A recursor for `AddOpposite`. Use as `induction x`."]
protected def rec' {F : αᵐᵒᵖ → Sort*} (h : ∀ X, F (op X)) : ∀ X, F X := fun X ↦ h (unop X)

Recursor for multiplicative opposite

Informal description

The recursor for the multiplicative opposite type $\alpha^\text{op}$ allows defining a function on $\alpha^\text{op}$ by specifying its behavior on elements of the form $\text{op}(X)$ for $X \in \alpha$. Given a function $h$ that defines the desired behavior on $\text{op}(X)$, the recursor extends this to all elements of $\alpha^\text{op}$.

MulOpposite.opEquiv definition

: α ≃ αᵐᵒᵖ

Full source

/-- The canonical bijection between `α` and `αᵐᵒᵖ`. -/
@[to_additive (attr := simps -fullyApplied apply symm_apply)
  "The canonical bijection between `α` and `αᵃᵒᵖ`."]
def opEquiv : α ≃ αᵐᵒᵖ :=
  ⟨op, unop, unop_op, op_unop⟩

Bijection between a type and its multiplicative opposite

Informal description

The bijection between a type $\alpha$ and its multiplicative opposite $\alpha^\text{op}$, consisting of the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$ and its inverse $\text{unop} : \alpha^\text{op} \to \alpha$, satisfying $\text{unop}(\text{op}(x)) = x$ for all $x \in \alpha$ and $\text{op}(\text{unop}(y)) = y$ for all $y \in \alpha^\text{op}$.

MulOpposite.op_bijective theorem

: Bijective (op : α → αᵐᵒᵖ)

Full source

@[to_additive]
theorem op_bijective : Bijective (op : α → αᵐᵒᵖ) :=
  opEquiv.bijective

Bijectivity of the Multiplicative Opposite Embedding

Informal description

The canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$ from a type $\alpha$ to its multiplicative opposite $\alpha^\text{op}$ is bijective. That is, it is both injective (distinct elements in $\alpha$ map to distinct elements in $\alpha^\text{op}$) and surjective (every element in $\alpha^\text{op}$ is the image of some element in $\alpha$).

MulOpposite.unop_bijective theorem

: Bijective (unop : αᵐᵒᵖ → α)

Full source

@[to_additive]
theorem unop_bijective : Bijective (unop : αᵐᵒᵖ → α) :=
  opEquiv.symm.bijective

Bijectivity of the Multiplicative Opposite Projection

Informal description

The canonical projection $\text{unop} : \alpha^\text{op} \to \alpha$ from the multiplicative opposite of $\alpha$ to $\alpha$ is bijective. That is, $\text{unop}$ is both injective (if $\text{unop}(x) = \text{unop}(y)$ then $x = y$) and surjective (for every $a \in \alpha$, there exists $b \in \alpha^\text{op}$ such that $\text{unop}(b) = a$).

MulOpposite.op_injective theorem

: Injective (op : α → αᵐᵒᵖ)

Full source

@[to_additive]
theorem op_injective : Injective (op : α → αᵐᵒᵖ) :=
  op_bijective.injective

Injectivity of the Multiplicative Opposite Embedding

Informal description

The canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$ from a type $\alpha$ to its multiplicative opposite $\alpha^\text{op}$ is injective. That is, for any $x, y \in \alpha$, if $\text{op}(x) = \text{op}(y)$, then $x = y$.

MulOpposite.op_surjective theorem

: Surjective (op : α → αᵐᵒᵖ)

Full source

@[to_additive]
theorem op_surjective : Surjective (op : α → αᵐᵒᵖ) :=
  op_bijective.surjective

Surjectivity of the Multiplicative Opposite Embedding

Informal description

The canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$ from a type $\alpha$ to its multiplicative opposite $\alpha^\text{op}$ is surjective. That is, for every element $y \in \alpha^\text{op}$, there exists an element $x \in \alpha$ such that $\text{op}(x) = y$.

MulOpposite.unop_injective theorem

: Injective (unop : αᵐᵒᵖ → α)

Full source

@[to_additive]
theorem unop_injective : Injective (unop : αᵐᵒᵖ → α) :=
  unop_bijective.injective

Injectivity of the Multiplicative Opposite Projection

Informal description

The canonical projection $\text{unop} : \alpha^\text{op} \to \alpha$ from the multiplicative opposite of $\alpha$ to $\alpha$ is injective. That is, for any $x, y \in \alpha^\text{op}$, if $\text{unop}(x) = \text{unop}(y)$, then $x = y$.

MulOpposite.unop_surjective theorem

: Surjective (unop : αᵐᵒᵖ → α)

Full source

@[to_additive]
theorem unop_surjective : Surjective (unop : αᵐᵒᵖ → α) :=
  unop_bijective.surjective

Surjectivity of the Multiplicative Opposite Projection

Informal description

The canonical projection $\text{unop} : \alpha^\text{op} \to \alpha$ from the multiplicative opposite of $\alpha$ to $\alpha$ is surjective. That is, for every $a \in \alpha$, there exists $b \in \alpha^\text{op}$ such that $\text{unop}(b) = a$.

MulOpposite.op_inj theorem

{x y : α} : op x = op y ↔ x = y

Full source

@[to_additive (attr := simp)]
theorem op_inj {x y : α} : opop x = op y ↔ x = y := iff_of_eq <| PreOpposite.op'.injEq _ _

Injectivity of the Multiplicative Opposite Embedding

Informal description

For any elements $x$ and $y$ of type $\alpha$, the canonical embeddings into the multiplicative opposite $\alpha^\text{op}$ satisfy $\text{op}(x) = \text{op}(y)$ if and only if $x = y$.

MulOpposite.unop_inj theorem

{x y : αᵐᵒᵖ} : unop x = unop y ↔ x = y

Full source

@[to_additive (attr := simp, nolint simpComm)]
theorem unop_inj {x y : αᵐᵒᵖ} : unopunop x = unop y ↔ x = y :=
  unop_injective.eq_iff

Injectivity of the Multiplicative Opposite Projection: $\text{unop}(x) = \text{unop}(y) \leftrightarrow x = y$

Informal description

For any elements $x$ and $y$ in the multiplicative opposite $\alpha^\text{op}$ of a type $\alpha$, the equality $\text{unop}(x) = \text{unop}(y)$ holds if and only if $x = y$. Here, $\text{unop} : \alpha^\text{op} \to \alpha$ is the canonical projection from the multiplicative opposite to the original type.

MulOpposite.forall theorem

{p : αᵐᵒᵖ → Prop} : (∀ a, p a) ↔ ∀ a, p (op a)

Full source

@[to_additive (attr := simp)] lemma «forall» {p : αᵐᵒᵖ → Prop} : (∀ a, p a) ↔ ∀ a, p (op a) :=
  op_surjective.forall

Universal Quantifier Equivalence via Multiplicative Opposite Embedding

Informal description

For any predicate $p$ on the multiplicative opposite $\alpha^\text{op}$ of a type $\alpha$, the statement $(\forall y \in \alpha^\text{op}, p(y))$ holds if and only if $(\forall x \in \alpha, p(\text{op}(x)))$ holds, where $\text{op} : \alpha \to \alpha^\text{op}$ is the canonical embedding.

MulOpposite.exists theorem

{p : αᵐᵒᵖ → Prop} : (∃ a, p a) ↔ ∃ a, p (op a)

Full source

@[to_additive (attr := simp)] lemma «exists» {p : αᵐᵒᵖ → Prop} : (∃ a, p a) ↔ ∃ a, p (op a) :=
  op_surjective.exists

Existence Transfer via Multiplicative Opposite Embedding

Informal description

For any predicate $p$ on the multiplicative opposite $\alpha^\text{op}$ of a type $\alpha$, there exists an element $a \in \alpha^\text{op}$ satisfying $p(a)$ if and only if there exists an element $a \in \alpha$ such that $p(\text{op}(a))$ holds, where $\text{op} : \alpha \to \alpha^\text{op}$ is the canonical embedding.

MulOpposite.instNontrivial instance

[Nontrivial α] : Nontrivial αᵐᵒᵖ

Full source

@[to_additive] instance instNontrivial [Nontrivial α] : Nontrivial αᵐᵒᵖ := op_injective.nontrivial

Nontriviality of Multiplicative Opposite

Informal description

For any nontrivial type $\alpha$, its multiplicative opposite $\alpha^\text{op}$ is also nontrivial.

MulOpposite.instInhabited instance

[Inhabited α] : Inhabited αᵐᵒᵖ

Full source

@[to_additive] instance instInhabited [Inhabited α] : Inhabited αᵐᵒᵖ := ⟨op default⟩

Inhabited Multiplicative Opposite

Informal description

For any inhabited type $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also inhabited. Specifically, if $a$ is an element of $\alpha$, then $\text{op}(a)$ is an element of $\alpha^\text{op}$.

MulOpposite.instSubsingleton instance

[Subsingleton α] : Subsingleton αᵐᵒᵖ

Full source

@[to_additive]
instance instSubsingleton [Subsingleton α] : Subsingleton αᵐᵒᵖ := unop_injective.subsingleton

Multiplicative Opposite Preserves Subsingleton Property

Informal description

For any type $\alpha$ that is a subsingleton (i.e., all elements of $\alpha$ are equal), its multiplicative opposite $\alpha^\text{op}$ is also a subsingleton.

MulOpposite.instUnique instance

[Unique α] : Unique αᵐᵒᵖ

Full source

@[to_additive] instance instUnique [Unique α] : Unique αᵐᵒᵖ := Unique.mk' _

Multiplicative Opposite Preserves Uniqueness

Informal description

For any type $\alpha$ with a unique element, the multiplicative opposite $\alpha^\text{op}$ also has a unique element.

MulOpposite.instIsEmpty instance

[IsEmpty α] : IsEmpty αᵐᵒᵖ

Full source

@[to_additive] instance instIsEmpty [IsEmpty α] : IsEmpty αᵐᵒᵖ := Function.isEmpty unop

Multiplicative Opposite Preserves Emptiness

Informal description

For any type $\alpha$, if $\alpha$ is empty, then its multiplicative opposite $\alpha^\text{op}$ is also empty.

MulOpposite.instDecidableEq instance

[DecidableEq α] : DecidableEq αᵐᵒᵖ

Full source

@[to_additive]
instance instDecidableEq [DecidableEq α] : DecidableEq αᵐᵒᵖ := unop_injective.decidableEq

Decidable Equality on the Multiplicative Opposite

Informal description

For any type $\alpha$ with decidable equality, the multiplicative opposite $\alpha^\text{op}$ also has decidable equality. Specifically, for any $x, y \in \alpha^\text{op}$, the equality $x = y$ can be decided by comparing their projections back to $\alpha$ via the canonical map $\text{unop} : \alpha^\text{op} \to \alpha$.

MulOpposite.instZero instance

[Zero α] : Zero αᵐᵒᵖ

Full source

instance instZero [Zero α] : Zero αᵐᵒᵖ where zero := op 0

Zero Element in the Multiplicative Opposite

Informal description

For any type $\alpha$ equipped with a zero element $0$, the multiplicative opposite $\alpha^\text{op}$ also has a zero element $\text{op}(0)$, where $\text{op} : \alpha \to \alpha^\text{op}$ is the canonical embedding.

MulOpposite.instOne instance

[One α] : One αᵐᵒᵖ

Full source

@[to_additive] instance instOne [One α] : One αᵐᵒᵖ where one := op 1

Multiplicative Identity in the Multiplicative Opposite

Informal description

For any type $\alpha$ equipped with a multiplicative identity element $1$, the multiplicative opposite $\alpha^\text{op}$ also has a multiplicative identity element $\text{op}(1)$, where $\text{op} : \alpha \to \alpha^\text{op}$ is the canonical embedding.

MulOpposite.instAdd instance

[Add α] : Add αᵐᵒᵖ

Full source

instance instAdd [Add α] : Add αᵐᵒᵖ where add x y := op (unop x + unop y)

Addition on the Multiplicative Opposite

Informal description

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

MulOpposite.instSub instance

[Sub α] : Sub αᵐᵒᵖ

Full source

instance instSub [Sub α] : Sub αᵐᵒᵖ where sub x y := op (unop x - unop y)

Subtraction on the Multiplicative Opposite

Informal description

For any type $\alpha$ equipped with a subtraction operation, the multiplicative opposite $\alpha^\text{op}$ inherits a subtraction operation where $\text{op}(x) - \text{op}(y) = \text{op}(x - y)$ for all $x, y \in \alpha$.

MulOpposite.instNeg instance

[Neg α] : Neg αᵐᵒᵖ

Full source

instance instNeg [Neg α] : Neg αᵐᵒᵖ where neg x := op <| -unop x

Negation on the Multiplicative Opposite

Informal description

For any type $\alpha$ equipped with a negation operation, the multiplicative opposite $\alpha^\text{op}$ inherits a negation operation where $\text{op}(-x) = -\text{op}(x)$ for all $x \in \alpha$.

MulOpposite.instInvolutiveNeg instance

[InvolutiveNeg α] : InvolutiveNeg αᵐᵒᵖ

Full source

instance instInvolutiveNeg [InvolutiveNeg α] : InvolutiveNeg αᵐᵒᵖ where
  neg_neg _ := unop_injective <| neg_neg _

Involutive Negation on the Multiplicative Opposite

Informal description

For any type $\alpha$ equipped with an involutive negation operation, the multiplicative opposite $\alpha^\text{op}$ also inherits an involutive negation operation. That is, for any $x \in \alpha$, the negation operation on $\alpha^\text{op}$ satisfies $-(\text{op}(x)) = \text{op}(-x)$ and $-(-\text{op}(x)) = \text{op}(x)$, where $\text{op} : \alpha \to \alpha^\text{op}$ is the canonical embedding.

MulOpposite.instMul instance

[Mul α] : Mul αᵐᵒᵖ

Full source

@[to_additive] instance instMul [Mul α] : Mul αᵐᵒᵖ where mul x y := op (unop y * unop x)

Multiplication on the Multiplicative Opposite

Informal description

For any type $\alpha$ equipped with a multiplication operation, the multiplicative opposite $\alpha^\text{op}$ inherits a multiplication operation defined by $\text{op}(x) \cdot \text{op}(y) = \text{op}(y \cdot x)$ for all $x, y \in \alpha$.

MulOpposite.instInv instance

[Inv α] : Inv αᵐᵒᵖ

Full source

@[to_additive] instance instInv [Inv α] : Inv αᵐᵒᵖ where inv x := op <| (unop x)⁻¹

Inversion on the Multiplicative Opposite

Informal description

For any type $\alpha$ equipped with an inversion operation, the multiplicative opposite $\alpha^\text{op}$ also inherits an inversion operation, where $\text{op}(x)^{-1} = \text{op}(x^{-1})$ for any $x \in \alpha$.

MulOpposite.instInvolutiveInv instance

[InvolutiveInv α] : InvolutiveInv αᵐᵒᵖ

Full source

@[to_additive]
instance instInvolutiveInv [InvolutiveInv α] : InvolutiveInv αᵐᵒᵖ where
  inv_inv _ := unop_injective <| inv_inv _

Involutive Inversion on the Multiplicative Opposite

Informal description

For any type $\alpha$ with an involutive inversion operation, the multiplicative opposite $\alpha^\text{op}$ also inherits an involutive inversion operation. That is, for any $x \in \alpha$, we have $\text{op}(x)^{-1} = \text{op}(x^{-1})$ and $\left(\text{op}(x)^{-1}\right)^{-1} = \text{op}(x)$.

MulOpposite.instSMul instance

[SMul α β] : SMul α βᵐᵒᵖ

Full source

@[to_additive] instance instSMul [SMul α β] : SMul α βᵐᵒᵖ where smul c x := op (c • unop x)

Scalar Multiplication on the Multiplicative Opposite

Informal description

For any type $\alpha$ with a scalar multiplication operation on a type $\beta$, the multiplicative opposite $\beta^\text{op}$ inherits a scalar multiplication operation from $\alpha$, where the action is defined by $a \cdot \text{op}(b) = \text{op}(a \cdot b)$ for any $a \in \alpha$ and $b \in \beta$.

MulOpposite.op_zero theorem

[Zero α] : op (0 : α) = 0

Full source

@[simp] lemma op_zero [Zero α] : op (0 : α) = 0 := rfl

Zero Preservation under Multiplicative Opposite Embedding

Informal description

For any type $\alpha$ with a zero element $0$, the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$ maps the zero element of $\alpha$ to the zero element of its multiplicative opposite $\alpha^\text{op}$, i.e., $\text{op}(0) = 0$.

MulOpposite.unop_zero theorem

[Zero α] : unop (0 : αᵐᵒᵖ) = 0

Full source

@[simp] lemma unop_zero [Zero α] : unop (0 : αᵐᵒᵖ) = 0 := rfl

Canonical Projection Preserves Zero in Multiplicative Opposite

Informal description

For any type $\alpha$ with a zero element $0$, the canonical projection from the multiplicative opposite $\alpha^\text{op}$ to $\alpha$ maps the zero element of $\alpha^\text{op}$ back to the zero element of $\alpha$, i.e., $\text{unop}(0) = 0$.

MulOpposite.op_one theorem

[One α] : op (1 : α) = 1

Full source

@[to_additive (attr := simp)] lemma op_one [One α] : op (1 : α) = 1 := rfl

Preservation of Multiplicative Identity under Multiplicative Opposite Embedding

Informal description

For any type $\alpha$ with a multiplicative identity element $1$, the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$ maps the identity element of $\alpha$ to the identity element of its multiplicative opposite $\alpha^\text{op}$, i.e., $\text{op}(1) = 1$.

MulOpposite.unop_one theorem

[One α] : unop (1 : αᵐᵒᵖ) = 1

Full source

@[to_additive (attr := simp)] lemma unop_one [One α] : unop (1 : αᵐᵒᵖ) = 1 := rfl

Projection Preserves Identity in Multiplicative Opposite

Informal description

For any type $\alpha$ with a multiplicative identity element $1$, the canonical projection from the multiplicative opposite $\alpha^\text{op}$ to $\alpha$ maps the identity element of $\alpha^\text{op}$ back to the identity element of $\alpha$, i.e., $\text{unop}(1) = 1$.

MulOpposite.op_add theorem

[Add α] (x y : α) : op (x + y) = op x + op y

Full source

@[simp] lemma op_add [Add α] (x y : α) : op (x + y) = op x + op y := rfl

Additivity of the Multiplicative Opposite's Canonical Map

Informal description

For any type $\alpha$ equipped with an addition operation, the canonical map $\text{op} : \alpha \to \alpha^\text{op}$ preserves addition, i.e., $\text{op}(x + y) = \text{op}(x) + \text{op}(y)$ for all $x, y \in \alpha$.

MulOpposite.unop_add theorem

[Add α] (x y : αᵐᵒᵖ) : unop (x + y) = unop x + unop y

Full source

@[simp] lemma unop_add [Add α] (x y : αᵐᵒᵖ) : unop (x + y) = unop x + unop y := rfl

Additivity of the Projection from Multiplicative Opposite

Informal description

For any type $\alpha$ with an addition operation, and for any elements $x, y$ in the multiplicative opposite $\alpha^\text{op}$, the projection back to $\alpha$ satisfies $\text{unop}(x + y) = \text{unop}(x) + \text{unop}(y)$.

MulOpposite.op_neg theorem

[Neg α] (x : α) : op (-x) = -op x

Full source

@[simp] lemma op_neg [Neg α] (x : α) : op (-x) = -op x := rfl

Negation Preservation in Multiplicative Opposite: $\text{op}(-x) = -\text{op}(x)$

Informal description

For any type $\alpha$ equipped with a negation operation and for any element $x \in \alpha$, the canonical map $\text{op} : \alpha \to \alpha^\text{op}$ satisfies $\text{op}(-x) = -\text{op}(x)$ in the multiplicative opposite $\alpha^\text{op}$.

MulOpposite.unop_neg theorem

[Neg α] (x : αᵐᵒᵖ) : unop (-x) = -unop x

Full source

@[simp] lemma unop_neg [Neg α] (x : αᵐᵒᵖ) : unop (-x) = -unop x := rfl

Negation Preservation under Projection from Multiplicative Opposite: $\text{unop}(-x) = -\text{unop}(x)$

Informal description

For any type $\alpha$ equipped with a negation operation and for any element $x$ in the multiplicative opposite $\alpha^\text{op}$, the projection $\text{unop}$ satisfies $\text{unop}(-x) = -\text{unop}(x)$ in $\alpha$.

MulOpposite.op_mul theorem

[Mul α] (x y : α) : op (x * y) = op y * op x

Full source

@[to_additive (attr := simp)] lemma op_mul [Mul α] (x y : α) : op (x * y) = op y * op x := rfl

Multiplication Reversal in Multiplicative Opposite: $\text{op}(x \cdot y) = \text{op}(y) \cdot \text{op}(x)$

Informal description

For any type $\alpha$ equipped with a multiplication operation and for any elements $x, y \in \alpha$, the canonical map $\text{op} : \alpha \to \alpha^\text{op}$ satisfies $\text{op}(x \cdot y) = \text{op}(y) \cdot \text{op}(x)$ in the multiplicative opposite $\alpha^\text{op}$.

MulOpposite.unop_mul theorem

[Mul α] (x y : αᵐᵒᵖ) : unop (x * y) = unop y * unop x

Full source

@[to_additive (attr := simp)]
lemma unop_mul [Mul α] (x y : αᵐᵒᵖ) : unop (x * y) = unop y * unop x := rfl

Projection Reverses Multiplication in Multiplicative Opposite: $\text{unop}(x \cdot y) = \text{unop}(y) \cdot \text{unop}(x)$

Informal description

For any type $\alpha$ equipped with a multiplication operation and for any elements $x, y$ in the multiplicative opposite $\alpha^\text{op}$, the projection $\text{unop}$ satisfies $\text{unop}(x \cdot y) = \text{unop}(y) \cdot \text{unop}(x)$ in $\alpha$.

MulOpposite.op_inv theorem

[Inv α] (x : α) : op x⁻¹ = (op x)⁻¹

Full source

@[to_additive (attr := simp)] lemma op_inv [Inv α] (x : α) : op x⁻¹ = (op x)⁻¹ := rfl

Inversion Commutes with Multiplicative Opposite Embedding: $\text{op}(x^{-1}) = (\text{op}(x))^{-1}$

Informal description

For any type $\alpha$ with an inversion operation and any element $x \in \alpha$, the canonical map to the multiplicative opposite satisfies $\text{op}(x^{-1}) = (\text{op}(x))^{-1}$.

MulOpposite.unop_inv theorem

[Inv α] (x : αᵐᵒᵖ) : unop x⁻¹ = (unop x)⁻¹

Full source

@[to_additive (attr := simp)] lemma unop_inv [Inv α] (x : αᵐᵒᵖ) : unop x⁻¹ = (unop x)⁻¹ := rfl

Inversion Commutes with Multiplicative Opposite Projection: $\text{unop}(x^{-1}) = (\text{unop}(x))^{-1}$

Informal description

For any type $\alpha$ with an inversion operation and any element $x$ in the multiplicative opposite $\alpha^\text{op}$, the projection $\text{unop}$ satisfies $\text{unop}(x^{-1}) = (\text{unop}(x))^{-1}$.

MulOpposite.op_sub theorem

[Sub α] (x y : α) : op (x - y) = op x - op y

Full source

@[simp] lemma op_sub [Sub α] (x y : α) : op (x - y) = op x - op y := rfl

Subtraction Preservation under Multiplicative Opposite Embedding

Informal description

For any type $\alpha$ equipped with a subtraction operation, and for any elements $x, y \in \alpha$, the canonical embedding into the multiplicative opposite satisfies $\text{op}(x - y) = \text{op}(x) - \text{op}(y)$.

MulOpposite.unop_sub theorem

[Sub α] (x y : αᵐᵒᵖ) : unop (x - y) = unop x - unop y

Full source

@[simp] lemma unop_sub [Sub α] (x y : αᵐᵒᵖ) : unop (x - y) = unop x - unop y := rfl

Subtraction Commutes with Multiplicative Opposite Projection

Informal description

For any type $\alpha$ equipped with a subtraction operation and for any elements $x, y$ in the multiplicative opposite $\alpha^\text{op}$, the projection $\text{unop}$ satisfies $\text{unop}(x - y) = \text{unop}(x) - \text{unop}(y)$.

MulOpposite.op_smul theorem

[SMul α β] (a : α) (b : β) : op (a • b) = a • op b

Full source

@[to_additive (attr := simp)]
lemma op_smul [SMul α β] (a : α) (b : β) : op (a • b) = a • op b := rfl

Scalar Multiplication Commutes with Multiplicative Opposite Embedding

Informal description

For any type $\alpha$ with a scalar multiplication operation on a type $\beta$, and for any elements $a \in \alpha$ and $b \in \beta$, the canonical embedding into the multiplicative opposite satisfies $\text{op}(a \cdot b) = a \cdot \text{op}(b)$, where $\text{op} : \beta \to \beta^\text{op}$ is the embedding and $\cdot$ denotes scalar multiplication.

MulOpposite.unop_smul theorem

[SMul α β] (a : α) (b : βᵐᵒᵖ) : unop (a • b) = a • unop b

Full source

@[to_additive (attr := simp)]
lemma unop_smul [SMul α β] (a : α) (b : βᵐᵒᵖ) : unop (a • b) = a • unop b := rfl

Scalar Multiplication Commutes with Multiplicative Opposite Projection

Informal description

For any type $\alpha$ with a scalar multiplication operation on a type $\beta$, and for any elements $a \in \alpha$ and $b \in \beta^\text{op}$, the projection from the multiplicative opposite satisfies $\text{unop}(a \cdot b) = a \cdot \text{unop}(b)$, where $\text{unop} : \beta^\text{op} \to \beta$ is the projection and $\cdot$ denotes scalar multiplication.

MulOpposite.unop_eq_zero_iff theorem

[Zero α] (a : αᵐᵒᵖ) : a.unop = (0 : α) ↔ a = (0 : αᵐᵒᵖ)

Full source

@[simp, nolint simpComm]
theorem unop_eq_zero_iff [Zero α] (a : αᵐᵒᵖ) : a.unop = (0 : α) ↔ a = (0 : αᵐᵒᵖ) :=
  unop_injective.eq_iff' rfl

Zero Preservation in Multiplicative Opposite: $\text{unop}(a) = 0 \leftrightarrow a = 0$

Informal description

For any type $\alpha$ with a zero element and any element $a$ in the multiplicative opposite $\alpha^\text{op}$, the projection $\text{unop}(a)$ equals $0$ in $\alpha$ if and only if $a$ equals $0$ in $\alpha^\text{op}$.

MulOpposite.op_eq_zero_iff theorem

[Zero α] (a : α) : op a = (0 : αᵐᵒᵖ) ↔ a = (0 : α)

Full source

@[simp]
theorem op_eq_zero_iff [Zero α] (a : α) : opop a = (0 : αᵐᵒᵖ) ↔ a = (0 : α) :=
  op_injective.eq_iff' rfl

Characterization of Zero in Multiplicative Opposite via Canonical Embedding

Informal description

For any type $\alpha$ with a zero element $0$ and any element $a \in \alpha$, the canonical embedding into the multiplicative opposite satisfies $\text{op}(a) = 0$ in $\alpha^\text{op}$ if and only if $a = 0$ in $\alpha$.

MulOpposite.unop_ne_zero_iff theorem

[Zero α] (a : αᵐᵒᵖ) : a.unop ≠ (0 : α) ↔ a ≠ (0 : αᵐᵒᵖ)

Full source

theorem unop_ne_zero_iff [Zero α] (a : αᵐᵒᵖ) : a.unop ≠ (0 : α)a.unop ≠ (0 : α) ↔ a ≠ (0 : αᵐᵒᵖ) :=
  not_congr <| unop_eq_zero_iff a

Nonzero Preservation in Multiplicative Opposite: $\text{unop}(a) \neq 0 \leftrightarrow a \neq 0$

Informal description

For any type $\alpha$ with a zero element and any element $a$ in the multiplicative opposite $\alpha^\text{op}$, the projection $\text{unop}(a)$ is nonzero in $\alpha$ if and only if $a$ is nonzero in $\alpha^\text{op}$.

MulOpposite.op_ne_zero_iff theorem

[Zero α] (a : α) : op a ≠ (0 : αᵐᵒᵖ) ↔ a ≠ (0 : α)

Full source

theorem op_ne_zero_iff [Zero α] (a : α) : opop a ≠ (0 : αᵐᵒᵖ)op a ≠ (0 : αᵐᵒᵖ) ↔ a ≠ (0 : α) :=
  not_congr <| op_eq_zero_iff a

Nonzero Characterization in Multiplicative Opposite: $\text{op}(a) \neq 0 \leftrightarrow a \neq 0$

Informal description

For any type $\alpha$ with a zero element $0$ and any element $a \in \alpha$, the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$ satisfies $\text{op}(a) \neq 0$ in $\alpha^\text{op}$ if and only if $a \neq 0$ in $\alpha$.

MulOpposite.unop_eq_one_iff theorem

[One α] (a : αᵐᵒᵖ) : a.unop = 1 ↔ a = 1

Full source

@[to_additive (attr := simp, nolint simpComm)]
theorem unop_eq_one_iff [One α] (a : αᵐᵒᵖ) : a.unop = 1 ↔ a = 1 :=
  unop_injective.eq_iff' rfl

Equivalence of Identity in Multiplicative Opposite and Original Type

Informal description

For any element $a$ in the multiplicative opposite $\alpha^\text{op}$ of a type $\alpha$ with a multiplicative identity $1$, the projection $\text{unop}(a)$ equals $1$ in $\alpha$ if and only if $a$ equals the identity element $1$ in $\alpha^\text{op}$.

MulOpposite.op_eq_one_iff theorem

[One α] (a : α) : op a = 1 ↔ a = 1

Full source

@[to_additive (attr := simp)]
lemma op_eq_one_iff [One α] (a : α) : opop a = 1 ↔ a = 1 := op_injective.eq_iff

Characterization of Multiplicative Identity in the Opposite Structure

Informal description

For any element $a$ in a type $\alpha$ with a multiplicative identity $1$, the canonical embedding $\text{op} : \alpha \to \alpha^\text{op}$ satisfies $\text{op}(a) = 1$ if and only if $a = 1$.

AddOpposite.instOne instance

[One α] : One αᵃᵒᵖ

Full source

instance instOne [One α] : One αᵃᵒᵖ where one := op 1

The Additive Opposite of a Type with One has One

Informal description

For any type $\alpha$ with a distinguished element $1$, the additive opposite $\alpha^{\text{aop}}$ also has a distinguished element $1$.

AddOpposite.op_one theorem

[One α] : op (1 : α) = 1

Full source

@[simp] lemma op_one [One α] : op (1 : α) = 1 := rfl

Preservation of multiplicative identity in additive opposite

Informal description

For any type $\alpha$ with a multiplicative identity element $1$, the canonical map $\text{op}$ from $\alpha$ to its additive opposite $\alpha^{\text{aop}}$ satisfies $\text{op}(1) = 1$.

AddOpposite.unop_one theorem

[One α] : unop 1 = (1 : α)

Full source

@[simp] lemma unop_one [One α] : unop 1 = (1 : α) := rfl

Inverse of Additive Opposite Preserves Multiplicative Identity

Informal description

For any type $\alpha$ with a multiplicative identity element $1$, the inverse of the canonical map from $\alpha$ to its additive opposite $\alpha^{\text{aop}}$ satisfies $\text{unop}(1) = 1$.

AddOpposite.op_eq_one_iff theorem

[One α] {a : α} : op a = 1 ↔ a = 1

Full source

@[simp] lemma op_eq_one_iff [One α] {a : α} : opop a = 1 ↔ a = 1 := op_injective.eq_iff

Characterization of Multiplicative Identity in Additive Opposite

Informal description

For any type $\alpha$ with a multiplicative identity element $1$, and for any element $a \in \alpha$, the canonical map $\text{op} : \alpha \to \alpha^{\text{aop}}$ satisfies $\text{op}(a) = 1$ if and only if $a = 1$.

AddOpposite.unop_eq_one_iff theorem

[One α] {a : αᵃᵒᵖ} : unop a = 1 ↔ a = 1

Full source

@[simp] lemma unop_eq_one_iff [One α] {a : αᵃᵒᵖ} : unopunop a = 1 ↔ a = 1 := unop_injective.eq_iff

Characterization of Multiplicative Identity in Additive Opposite via Unop

Informal description

For any type $\alpha$ with a multiplicative identity element $1$, and for any element $a$ in the additive opposite $\alpha^{\text{aop}}$, the inverse of the canonical map satisfies $\text{unop}(a) = 1$ if and only if $a = 1$.

AddOpposite.instMul instance

[Mul α] : Mul αᵃᵒᵖ

Full source

instance instMul [Mul α] : Mul αᵃᵒᵖ where mul a b := op (unop a * unop b)

Multiplication on the Additive Opposite

Informal description

For any type $\alpha$ equipped with a multiplication operation, the additive opposite $\alpha^{\text{aop}}$ also carries a multiplication operation, where the product of two elements in $\alpha^{\text{aop}}$ corresponds to the product of their underlying elements in $\alpha$.

AddOpposite.op_mul theorem

[Mul α] (a b : α) : op (a * b) = op a * op b

Full source

@[simp] lemma op_mul [Mul α] (a b : α) : op (a * b) = op a * op b := rfl

Multiplication Preservation by Additive Opposite Map

Informal description

For any type $\alpha$ with a multiplication operation, the canonical map $\text{op}$ from $\alpha$ to its additive opposite $\alpha^{\text{aop}}$ preserves multiplication. That is, for any elements $a, b \in \alpha$, we have $\text{op}(a * b) = \text{op}(a) * \text{op}(b)$.

AddOpposite.unop_mul theorem

[Mul α] (a b : αᵃᵒᵖ) : unop (a * b) = unop a * unop b

Full source

@[simp] lemma unop_mul [Mul α] (a b : αᵃᵒᵖ) : unop (a * b) = unop a * unop b := rfl

Underlying Product in Additive Opposite Equals Product of Underlying Elements

Informal description

For any type $\alpha$ with a multiplication operation, and for any elements $a, b$ in the additive opposite $\alpha^{\text{aop}}$, the underlying element of the product $a * b$ in $\alpha^{\text{aop}}$ is equal to the product of the underlying elements of $a$ and $b$ in $\alpha$, i.e., $\text{unop}(a * b) = \text{unop}(a) * \text{unop}(b)$.

AddOpposite.instInv instance

[Inv α] : Inv αᵃᵒᵖ

Full source

instance instInv [Inv α] : Inv αᵃᵒᵖ where inv a := op (unop a)⁻¹

Inversion on Additive Opposite

Informal description

For any type $\alpha$ with an inversion operation $⁻¹$, the additive opposite $\alphaᵃᵒᵖ$ also has an inversion operation defined by $(op\ a)⁻¹ = op\ (a⁻¹)$.

AddOpposite.instInvolutiveInv instance

[InvolutiveInv α] : InvolutiveInv αᵃᵒᵖ

Full source

instance instInvolutiveInv [InvolutiveInv α] : InvolutiveInv αᵃᵒᵖ where
  inv_inv _ := unop_injective <| inv_inv _

Involutive Inversion on Additive Opposite

Informal description

For any type $\alpha$ with an involutive inversion operation $⁻¹$ (i.e., satisfying $(a⁻¹)⁻¹ = a$ for all $a \in \alpha$), the additive opposite $\alpha^{\text{aop}}$ also inherits an involutive inversion operation.

AddOpposite.op_inv theorem

[Inv α] (a : α) : op a⁻¹ = (op a)⁻¹

Full source

@[simp] lemma op_inv [Inv α] (a : α) : op a⁻¹ = (op a)⁻¹ := rfl

Inversion Commutes with Canonical Map to Additive Opposite

Informal description

For any type $\alpha$ with an inversion operation $⁻¹$ and any element $a \in \alpha$, the canonical map $\text{op} : \alpha \to \alpha^\text{op}$ satisfies $\text{op}(a⁻¹) = (\text{op}(a))⁻¹$.

AddOpposite.unop_inv theorem

[Inv α] (a : αᵃᵒᵖ) : unop a⁻¹ = (unop a)⁻¹

Full source

@[simp] lemma unop_inv [Inv α] (a : αᵃᵒᵖ) : unop a⁻¹ = (unop a)⁻¹ := rfl

Inversion Commutes with Unary Operation in Additive Opposite

Informal description

For any type $\alpha$ with an inversion operation $⁻¹$ and any element $a$ in the additive opposite $\alpha^\text{op}$, the unary operation $\text{unop}$ satisfies $\text{unop}(a⁻¹) = (\text{unop}(a))⁻¹$.

AddOpposite.instDiv instance

[Div α] : Div αᵃᵒᵖ

Full source

instance instDiv [Div α] : Div αᵃᵒᵖ where div a b := op (unop a / unop b)

Division Operation on Additive Opposite

Informal description

For any type $\alpha$ equipped with a division operation, the additive opposite $\alpha^\text{op}$ also inherits a division operation. This operation is defined such that the canonical map $\text{op} : \alpha \to \alpha^\text{op}$ preserves division, i.e., $\text{op}(a / b) = \text{op}(a) / \text{op}(b)$ for all $a, b \in \alpha$.

AddOpposite.op_div theorem

[Div α] (a b : α) : op (a / b) = op a / op b

Full source

@[simp] lemma op_div [Div α] (a b : α) : op (a / b) = op a / op b := rfl

Canonical Map Preserves Division in Additive Opposite

Informal description

For any type $\alpha$ equipped with a division operation and any elements $a, b \in \alpha$, the canonical map $\text{op} : \alpha \to \alpha^\text{op}$ satisfies $\text{op}(a / b) = \text{op}(a) / \text{op}(b)$.

AddOpposite.unop_div theorem

[Div α] (a b : αᵃᵒᵖ) : unop (a / b) = unop a / unop b

Full source

@[simp] lemma unop_div [Div α] (a b : αᵃᵒᵖ) : unop (a / b) = unop a / unop b := rfl

Unary Operation Preserves Division in Additive Opposite

Informal description

For any type $\alpha$ with a division operation and any elements $a, b$ in the additive opposite $\alpha^\text{op}$, the unary operation $\text{unop}$ satisfies $\text{unop}(a / b) = \text{unop}(a) / \text{unop}(b)$.

Mathlib.Algebra.Opposites

Notation

Implementation notes

Tags