Multiplicative opposite and algebraic operations on it #
In this file we define MulOpposite α = αᵐᵒᵖ
to be the multiplicative opposite of α
. It inherits
all additive algebraic structures on α
(in other files), and reverses the order of multipliers in
multiplicative structures, i.e., op (x * y) = op y * op x
, where MulOpposite.op
is the
canonical map from α
to αᵐᵒᵖ
.
We also define AddOpposite α = αᵃᵒᵖ
to be the additive opposite of α
. It inherits all
multiplicative algebraic structures on α
(in other files), and reverses the order of summands in
additive structures, i.e. op (x + y) = op y + op x
, where AddOpposite.op
is the canonical map
from α
to αᵃᵒᵖ
.
Notation #
αᵐᵒᵖ = MulOpposite α
αᵃᵒᵖ = AddOpposite α
Implementation notes #
In mathlib3 αᵐᵒᵖ
was just a type synonym for α
, marked irreducible after the API
was developed. In mathlib4 we use a structure with one field, because it is not possible
to change the reducibility of a declaration after its definition, and because Lean 4 has
definitional eta reduction for structures (Lean 3 does not).
Tags #
multiplicative opposite, additive opposite
- op' :: (
- unop' : α
The element of
α
represented byx : PreOpposite α
. - )
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 mathlib4#1036).
Instances For
Additive opposite of a type. This type inherits all multiplicative structures on α
and
reverses left and right in addition.
Instances For
Multiplicative opposite of a type. This type inherits all additive structures on α
and
reverses left and right in multiplication.
Instances For
The element of αᵃᵒᵖ
that represents x : α
.
Instances For
The element of MulOpposite α
that represents x : α
.
Instances For
The element of α
represented by x : αᵃᵒᵖ
.
Instances For
The element of α
represented by x : αᵐᵒᵖ
.
Instances For
A recursor for AddOpposite
. Use as induction x using AddOpposite.rec'
.
Instances For
A recursor for MulOpposite
. Use as induction x using MulOpposite.rec'
.
Instances For
The canonical bijection between α
and αᵃᵒᵖ
.
Instances For
The canonical bijection between α
and αᵐᵒᵖ
.