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 :: (
The element of
α
represented byx : αᵐᵒᵖ
.unop : α- )
Multiplicative opposite of a type. This type inherits all additive structures on α
and
reverses left and right in multiplication.
Instances For
- op :: (
The element of
α
represented byx : αᵃᵒᵖ
.unop : α- )
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.
Equations
- «term_ᵐᵒᵖ» = Lean.ParserDescr.trailingNode `term_ᵐᵒᵖ 1024 1024 (Lean.ParserDescr.symbol "ᵐᵒᵖ")
Additive opposite of a type.
Equations
- «term_ᵃᵒᵖ» = Lean.ParserDescr.trailingNode `term_ᵃᵒᵖ 1024 1024 (Lean.ParserDescr.symbol "ᵃᵒᵖ")
A recursor for AddOpposite
. Use as induction x using AddOpposite.rec
.
Equations
- AddOpposite.rec' h X = h X.unop
A recursor for MulOpposite
. Use as induction x using MulOpposite.rec'
.
Equations
- MulOpposite.rec' h X = h X.unop
Equations
- (_ : Nontrivial αᵃᵒᵖ) = (_ : Nontrivial αᵃᵒᵖ)
Equations
- AddOpposite.inhabited α = { default := { unop := default } }
Equations
- MulOpposite.inhabited α = { default := { unop := default } }
Equations
- (_ : Subsingleton αᵃᵒᵖ) = (_ : Subsingleton αᵃᵒᵖ)
Equations
Equations
- (_ : Subsingleton αᵃᵒᵖ) = (_ : Subsingleton αᵃᵒᵖ)
Equations
Equations
- MulOpposite.zero α = { zero := { unop := 0 } }
Equations
- AddOpposite.zero α = { zero := { unop := 0 } }
Equations
- MulOpposite.one α = { one := { unop := 1 } }
Equations
- MulOpposite.add α = { add := fun x y => { unop := x.unop + y.unop } }
Equations
- MulOpposite.sub α = { sub := fun x y => { unop := x.unop - y.unop } }
Equations
- MulOpposite.neg α = { neg := fun x => { unop := -x.unop } }
Equations
- MulOpposite.involutiveNeg α = let src := MulOpposite.neg α; InvolutiveNeg.mk (_ : ∀ (x : αᵐᵒᵖ), - -x = x)
Equations
- AddOpposite.add α = { add := fun x y => { unop := y.unop + x.unop } }
Equations
- MulOpposite.mul α = { mul := fun x y => { unop := y.unop * x.unop } }
Equations
- AddOpposite.neg α = { neg := fun x => { unop := -x.unop } }
Equations
- MulOpposite.inv α = { inv := fun x => { unop := x.unop⁻¹ } }
Equations
- AddOpposite.involutiveNeg α = let src := AddOpposite.neg α; InvolutiveNeg.mk (_ : ∀ (x : αᵃᵒᵖ), - -x = x)
Equations
- MulOpposite.involutiveInv α = let src := MulOpposite.inv α; InvolutiveInv.mk (_ : ∀ (x : αᵐᵒᵖ), x⁻¹⁻¹ = x)