algebra.opposites - mathlib docs

@[irreducible]

def mul_opposite (α : Type u) :

Type u

Multiplicative opposite of a type. This type inherits all additive structures on α and reverses left and right in multiplication.

Equations

αᵐᵒᵖ = α

Instances for mul_opposite

source

def add_opposite (α : Type u) :

Type u

Additive opposite of a type. This type inherits all multiplicative structures on α and reverses left and right in addition.

Equations

αᵃᵒᵖ = α

Instances for add_opposite

source

def mul_opposite.op {α : Type u} :

α → αᵐᵒᵖ

The element of mul_opposite α that represents x : α.

Equations

mul_opposite.op = id

source

def add_opposite.op {α : Type u} :

α → αᵃᵒᵖ

The element of αᵃᵒᵖ that represents x : α.

Equations

add_opposite.op = id

source

def mul_opposite.unop {α : Type u} :

αᵐᵒᵖ → α

The element of α represented by x : αᵐᵒᵖ.

Equations

mul_opposite.unop = id

source

def add_opposite.unop {α : Type u} :

αᵃᵒᵖ → α

The element of α represented by x : αᵃᵒᵖ.

Equations

add_opposite.unop = id

source

@[simp]

theorem mul_opposite.unop_op {α : Type u} (x : α) :

mul_opposite.unop (mul_opposite.op x) = x

source

@[simp]

theorem add_opposite.unop_op {α : Type u} (x : α) :

add_opposite.unop (add_opposite.op x) = x

source

@[simp]

theorem mul_opposite.op_unop {α : Type u} (x : αᵐᵒᵖ) :

mul_opposite.op (mul_opposite.unop x) = x

source

@[simp]

theorem add_opposite.op_unop {α : Type u} (x : αᵃᵒᵖ) :

add_opposite.op (add_opposite.unop x) = x

source

@[simp]

theorem add_opposite.op_comp_unop {α : Type u} :

add_opposite.op ∘ add_opposite.unop = id

source

@[simp]

theorem mul_opposite.op_comp_unop {α : Type u} :

mul_opposite.op ∘ mul_opposite.unop = id

source

@[simp]

theorem mul_opposite.unop_comp_op {α : Type u} :

mul_opposite.unop ∘ mul_opposite.op = id

source

@[simp]

theorem add_opposite.unop_comp_op {α : Type u} :

add_opposite.unop ∘ add_opposite.op = id

source

@[protected, simp]

def mul_opposite.rec {α : Type u} {F : αᵐᵒᵖ → Sort v} (h : Π (X : α), F (mul_opposite.op X)) (X : αᵐᵒᵖ) :

F X

A recursor for mul_opposite. Use as induction x using mul_opposite.rec.

Equations

mul_opposite.rec h = λ (X : αᵐᵒᵖ), h (mul_opposite.unop X)

source

@[protected, simp]

def add_opposite.rec {α : Type u} {F : αᵃᵒᵖ → Sort v} (h : Π (X : α), F (add_opposite.op X)) (X : αᵃᵒᵖ) :

F X

A recursor for add_opposite. Use as induction x using add_opposite.rec.

Equations

add_opposite.rec h = λ (X : αᵃᵒᵖ), h (add_opposite.unop X)

source

@[simp]

theorem mul_opposite.op_equiv_apply {α : Type u} :

⇑mul_opposite.op_equiv = mul_opposite.op

source

def mul_opposite.op_equiv {α : Type u} :

α ≃ αᵐᵒᵖ

The canonical bijection between α and αᵐᵒᵖ.

Equations

mul_opposite.op_equiv = {to_fun := mul_opposite.op α, inv_fun := mul_opposite.unop α, left_inv := _, right_inv := _}

source

@[simp]

theorem add_opposite.op_equiv_apply {α : Type u} :

⇑add_opposite.op_equiv = add_opposite.op

source

@[simp]

theorem add_opposite.op_equiv_symm_apply {α : Type u} :

⇑(add_opposite.op_equiv.symm) = add_opposite.unop

source

@[simp]

theorem mul_opposite.op_equiv_symm_apply {α : Type u} :

⇑(mul_opposite.op_equiv.symm) = mul_opposite.unop

source

def add_opposite.op_equiv {α : Type u} :

α ≃ αᵃᵒᵖ

The canonical bijection between α and αᵃᵒᵖ.

Equations

add_opposite.op_equiv = {to_fun := add_opposite.op α, inv_fun := add_opposite.unop α, left_inv := _, right_inv := _}

source

theorem mul_opposite.op_bijective {α : Type u} :

function.bijective mul_opposite.op

source

theorem add_opposite.op_bijective {α : Type u} :

function.bijective add_opposite.op

source

theorem mul_opposite.unop_bijective {α : Type u} :

function.bijective mul_opposite.unop

source

theorem add_opposite.unop_bijective {α : Type u} :

function.bijective add_opposite.unop

source

theorem mul_opposite.op_injective {α : Type u} :

function.injective mul_opposite.op

source

theorem add_opposite.op_injective {α : Type u} :

function.injective add_opposite.op

source

theorem add_opposite.op_surjective {α : Type u} :

function.surjective add_opposite.op

source

theorem mul_opposite.op_surjective {α : Type u} :

function.surjective mul_opposite.op

source

theorem mul_opposite.unop_injective {α : Type u} :

function.injective mul_opposite.unop

source

theorem add_opposite.unop_injective {α : Type u} :

function.injective add_opposite.unop

source

theorem mul_opposite.unop_surjective {α : Type u} :

function.surjective mul_opposite.unop

source

theorem add_opposite.unop_surjective {α : Type u} :

function.surjective add_opposite.unop

source

@[simp]

theorem add_opposite.op_inj {α : Type u} {x y : α} :

add_opposite.op x = add_opposite.op y ↔ x = y

source

@[simp]

theorem mul_opposite.op_inj {α : Type u} {x y : α} :

mul_opposite.op x = mul_opposite.op y ↔ x = y

source

@[simp]

theorem add_opposite.unop_inj {α : Type u} {x y : αᵃᵒᵖ} :

add_opposite.unop x = add_opposite.unop y ↔ x = y

source

@[simp]

theorem mul_opposite.unop_inj {α : Type u} {x y : αᵐᵒᵖ} :

mul_opposite.unop x = mul_opposite.unop y ↔ x = y

source

@[protected, instance]

def mul_opposite.nontrivial (α : Type u) [nontrivial α] :

nontrivial αᵐᵒᵖ

source

@[protected, instance]

def add_opposite.nontrivial (α : Type u) [nontrivial α] :

nontrivial αᵃᵒᵖ

source

@[protected, instance]

def add_opposite.inhabited (α : Type u) [inhabited α] :

inhabited αᵃᵒᵖ

Equations

add_opposite.inhabited α = {default := add_opposite.op inhabited.default}

source

@[protected, instance]

def mul_opposite.inhabited (α : Type u) [inhabited α] :

inhabited αᵐᵒᵖ

Equations

mul_opposite.inhabited α = {default := mul_opposite.op inhabited.default}

source

@[protected, instance]

def mul_opposite.subsingleton (α : Type u) [subsingleton α] :

subsingleton αᵐᵒᵖ

source

@[protected, instance]

def add_opposite.subsingleton (α : Type u) [subsingleton α] :

subsingleton αᵃᵒᵖ

source

@[protected, instance]

def add_opposite.unique (α : Type u) [unique α] :

unique αᵃᵒᵖ

Equations

add_opposite.unique α = unique.mk' αᵃᵒᵖ

source

@[protected, instance]

def mul_opposite.unique (α : Type u) [unique α] :

unique αᵐᵒᵖ

Equations

mul_opposite.unique α = unique.mk' αᵐᵒᵖ

source

@[protected, instance]

def mul_opposite.is_empty (α : Type u) [is_empty α] :

is_empty αᵐᵒᵖ

source

@[protected, instance]

def add_opposite.is_empty (α : Type u) [is_empty α] :

is_empty αᵃᵒᵖ

source

@[protected, instance]

def mul_opposite.has_zero (α : Type u) [has_zero α] :

has_zero αᵐᵒᵖ

Equations

mul_opposite.has_zero α = {zero := mul_opposite.op 0}

source

@[protected, instance]

def mul_opposite.has_one (α : Type u) [has_one α] :

has_one αᵐᵒᵖ

Equations

mul_opposite.has_one α = {one := mul_opposite.op 1}

source

@[protected, instance]

def add_opposite.has_zero (α : Type u) [has_zero α] :

has_zero αᵃᵒᵖ

Equations

add_opposite.has_zero α = {zero := add_opposite.op 0}

source

@[protected, instance]

def mul_opposite.has_add (α : Type u) [has_add α] :

has_add αᵐᵒᵖ

Equations

mul_opposite.has_add α = {add := λ (x y : αᵐᵒᵖ), mul_opposite.op (mul_opposite.unop x + mul_opposite.unop y)}

source

@[protected, instance]

def mul_opposite.has_sub (α : Type u) [has_sub α] :

has_sub αᵐᵒᵖ

Equations

mul_opposite.has_sub α = {sub := λ (x y : αᵐᵒᵖ), mul_opposite.op (mul_opposite.unop x - mul_opposite.unop y)}

source

@[protected, instance]

def mul_opposite.has_neg (α : Type u) [has_neg α] :

has_neg αᵐᵒᵖ

Equations

mul_opposite.has_neg α = {neg := λ (x : αᵐᵒᵖ), mul_opposite.op (-mul_opposite.unop x)}

source

@[protected, instance]

def mul_opposite.has_involutive_neg (α : Type u) [has_involutive_neg α] :

has_involutive_neg αᵐᵒᵖ

Equations

mul_opposite.has_involutive_neg α = {neg := has_neg.neg (mul_opposite.has_neg α), neg_neg := _}

source

@[protected, instance]

def add_opposite.has_add (α : Type u) [has_add α] :

has_add αᵃᵒᵖ

Equations

add_opposite.has_add α = {add := λ (x y : αᵃᵒᵖ), add_opposite.op (add_opposite.unop y + add_opposite.unop x)}

source

@[protected, instance]

def mul_opposite.has_mul (α : Type u) [has_mul α] :

has_mul αᵐᵒᵖ

Equations

mul_opposite.has_mul α = {mul := λ (x y : αᵐᵒᵖ), mul_opposite.op (mul_opposite.unop y * mul_opposite.unop x)}

source

@[protected, instance]

def mul_opposite.has_inv (α : Type u) [has_inv α] :

has_inv αᵐᵒᵖ

Equations

mul_opposite.has_inv α = {inv := λ (x : αᵐᵒᵖ), mul_opposite.op (mul_opposite.unop x)⁻¹}

source

@[protected, instance]

def add_opposite.has_neg (α : Type u) [has_neg α] :

has_neg αᵃᵒᵖ

Equations

add_opposite.has_neg α = {neg := λ (x : αᵃᵒᵖ), add_opposite.op (-add_opposite.unop x)}

source

@[protected, instance]

def mul_opposite.has_involutive_inv (α : Type u) [has_involutive_inv α] :

has_involutive_inv αᵐᵒᵖ

Equations

mul_opposite.has_involutive_inv α = {inv := has_inv.inv (mul_opposite.has_inv α), inv_inv := _}

source

@[protected, instance]

def add_opposite.has_involutive_neg (α : Type u) [has_involutive_neg α] :

has_involutive_neg αᵃᵒᵖ

Equations

add_opposite.has_involutive_neg α = {neg := has_neg.neg (add_opposite.has_neg α), neg_neg := _}

source

@[protected, instance]

def add_opposite.has_vadd (α : Type u) (R : Type u_1) [has_vadd R α] :

has_vadd R αᵃᵒᵖ

Equations

add_opposite.has_vadd α R = {vadd := λ (c : R) (x : αᵃᵒᵖ), add_opposite.op (c +ᵥ add_opposite.unop x)}

source

@[protected, instance]

def mul_opposite.has_smul (α : Type u) (R : Type u_1) [has_smul R α] :

has_smul R αᵐᵒᵖ

Equations

mul_opposite.has_smul α R = {smul := λ (c : R) (x : αᵐᵒᵖ), mul_opposite.op (c • mul_opposite.unop x)}

source

@[simp]

theorem mul_opposite.op_zero (α : Type u) [has_zero α] :

mul_opposite.op 0 = 0

source

@[simp]

theorem mul_opposite.unop_zero (α : Type u) [has_zero α] :

mul_opposite.unop 0 = 0

source

@[simp]

theorem add_opposite.op_zero (α : Type u) [has_zero α] :

add_opposite.op 0 = 0

source

@[simp]

theorem mul_opposite.op_one (α : Type u) [has_one α] :

mul_opposite.op 1 = 1

source

@[simp]

theorem mul_opposite.unop_one (α : Type u) [has_one α] :

mul_opposite.unop 1 = 1

source

@[simp]

theorem add_opposite.unop_zero (α : Type u) [has_zero α] :

add_opposite.unop 0 = 0

source

@[simp]

theorem mul_opposite.op_add {α : Type u} [has_add α] (x y : α) :

mul_opposite.op (x + y) = mul_opposite.op x + mul_opposite.op y

source

@[simp]

theorem mul_opposite.unop_add {α : Type u} [has_add α] (x y : αᵐᵒᵖ) :

mul_opposite.unop (x + y) = mul_opposite.unop x + mul_opposite.unop y

source

@[simp]

theorem mul_opposite.op_neg {α : Type u} [has_neg α] (x : α) :

mul_opposite.op (-x) = -mul_opposite.op x

source

@[simp]

theorem mul_opposite.unop_neg {α : Type u} [has_neg α] (x : αᵐᵒᵖ) :

mul_opposite.unop (-x) = -mul_opposite.unop x

source

@[simp]

theorem add_opposite.op_add {α : Type u} [has_add α] (x y : α) :

add_opposite.op (x + y) = add_opposite.op y + add_opposite.op x

source

@[simp]

theorem mul_opposite.op_mul {α : Type u} [has_mul α] (x y : α) :

mul_opposite.op (x * y) = mul_opposite.op y * mul_opposite.op x

source

@[simp]

theorem mul_opposite.unop_mul {α : Type u} [has_mul α] (x y : αᵐᵒᵖ) :

mul_opposite.unop (x * y) = mul_opposite.unop y * mul_opposite.unop x

source

@[simp]

theorem add_opposite.unop_add {α : Type u} [has_add α] (x y : αᵃᵒᵖ) :

add_opposite.unop (x + y) = add_opposite.unop y + add_opposite.unop x

source

@[simp]

theorem add_opposite.op_neg {α : Type u} [has_neg α] (x : α) :

add_opposite.op (-x) = -add_opposite.op x

source

@[simp]

theorem mul_opposite.op_inv {α : Type u} [has_inv α] (x : α) :

mul_opposite.op x⁻¹ = (mul_opposite.op x)⁻¹

source

@[simp]

theorem mul_opposite.unop_inv {α : Type u} [has_inv α] (x : αᵐᵒᵖ) :

mul_opposite.unop x⁻¹ = (mul_opposite.unop x)⁻¹

source

@[simp]

theorem add_opposite.unop_neg {α : Type u} [has_neg α] (x : αᵃᵒᵖ) :

add_opposite.unop (-x) = -add_opposite.unop x

source

@[simp]

theorem mul_opposite.op_sub {α : Type u} [has_sub α] (x y : α) :

mul_opposite.op (x - y) = mul_opposite.op x - mul_opposite.op y

source

@[simp]

theorem mul_opposite.unop_sub {α : Type u} [has_sub α] (x y : αᵐᵒᵖ) :

mul_opposite.unop (x - y) = mul_opposite.unop x - mul_opposite.unop y

source

@[simp]

theorem add_opposite.op_vadd {α : Type u} {R : Type u_1} [has_vadd R α] (c : R) (a : α) :

add_opposite.op (c +ᵥ a) = c +ᵥ add_opposite.op a

source

@[simp]

theorem mul_opposite.op_smul {α : Type u} {R : Type u_1} [has_smul R α] (c : R) (a : α) :

mul_opposite.op (c • a) = c • mul_opposite.op a

source

@[simp]

theorem mul_opposite.unop_smul {α : Type u} {R : Type u_1} [has_smul R α] (c : R) (a : αᵐᵒᵖ) :

mul_opposite.unop (c • a) = c • mul_opposite.unop a

source

@[simp]

theorem add_opposite.unop_vadd {α : Type u} {R : Type u_1} [has_vadd R α] (c : R) (a : αᵃᵒᵖ) :

add_opposite.unop (c +ᵥ a) = c +ᵥ add_opposite.unop a

source

@[simp]

theorem mul_opposite.unop_eq_zero_iff {α : Type u} [has_zero α] (a : αᵐᵒᵖ) :

mul_opposite.unop a = 0 ↔ a = 0

source

@[simp]

theorem mul_opposite.op_eq_zero_iff {α : Type u} [has_zero α] (a : α) :

mul_opposite.op a = 0 ↔ a = 0

source

theorem mul_opposite.unop_ne_zero_iff {α : Type u} [has_zero α] (a : αᵐᵒᵖ) :

mul_opposite.unop a ≠ 0 ↔ a ≠ 0

source

theorem mul_opposite.op_ne_zero_iff {α : Type u} [has_zero α] (a : α) :

mul_opposite.op a ≠ 0 ↔ a ≠ 0

source

@[simp]

theorem mul_opposite.unop_eq_one_iff {α : Type u} [has_one α] (a : αᵐᵒᵖ) :

mul_opposite.unop a = 1 ↔ a = 1

source

@[simp]

theorem add_opposite.unop_eq_zero_iff {α : Type u} [has_zero α] (a : αᵃᵒᵖ) :

add_opposite.unop a = 0 ↔ a = 0

source

@[simp]

theorem add_opposite.op_eq_zero_iff {α : Type u} [has_zero α] (a : α) :

add_opposite.op a = 0 ↔ a = 0

source

@[simp]

theorem mul_opposite.op_eq_one_iff {α : Type u} [has_one α] (a : α) :

mul_opposite.op a = 1 ↔ a = 1

source

@[protected, instance]

def add_opposite.has_one {α : Type u} [has_one α] :

has_one αᵃᵒᵖ

Equations

add_opposite.has_one = {one := add_opposite.op 1}

source

@[simp]

theorem add_opposite.op_one {α : Type u} [has_one α] :

add_opposite.op 1 = 1

source

@[simp]

theorem add_opposite.unop_one {α : Type u} [has_one α] :

add_opposite.unop 1 = 1

source

@[simp]

theorem add_opposite.op_eq_one_iff {α : Type u} [has_one α] {a : α} :

add_opposite.op a = 1 ↔ a = 1

source

@[simp]

theorem add_opposite.unop_eq_one_iff {α : Type u} [has_one α] {a : αᵃᵒᵖ} :

add_opposite.unop a = 1 ↔ a = 1

source

@[protected, instance]

def add_opposite.has_mul {α : Type u} [has_mul α] :

has_mul αᵃᵒᵖ

Equations

add_opposite.has_mul = {mul := λ (a b : αᵃᵒᵖ), add_opposite.op (add_opposite.unop a * add_opposite.unop b)}

source

@[simp]

theorem add_opposite.op_mul {α : Type u} [has_mul α] (a b : α) :

add_opposite.op (a * b) = add_opposite.op a * add_opposite.op b

source

@[simp]

theorem add_opposite.unop_mul {α : Type u} [has_mul α] (a b : αᵃᵒᵖ) :

add_opposite.unop (a * b) = add_opposite.unop a * add_opposite.unop b

source

@[protected, instance]

def add_opposite.has_inv {α : Type u} [has_inv α] :

has_inv αᵃᵒᵖ

Equations

add_opposite.has_inv = {inv := λ (a : αᵃᵒᵖ), add_opposite.op (add_opposite.unop a)⁻¹}

source

@[protected, instance]

def add_opposite.has_involutive_inv {α : Type u} [has_involutive_inv α] :

has_involutive_inv αᵃᵒᵖ

Equations

add_opposite.has_involutive_inv = {inv := has_inv.inv add_opposite.has_inv, inv_inv := _}

source

@[simp]

theorem add_opposite.op_inv {α : Type u} [has_inv α] (a : α) :

add_opposite.op a⁻¹ = (add_opposite.op a)⁻¹

source

@[simp]

theorem add_opposite.unop_inv {α : Type u} [has_inv α] (a : αᵃᵒᵖ) :

add_opposite.unop a⁻¹ = (add_opposite.unop a)⁻¹

source

@[protected, instance]

def add_opposite.has_div {α : Type u} [has_div α] :

has_div αᵃᵒᵖ

Equations

add_opposite.has_div = {div := λ (a b : αᵃᵒᵖ), add_opposite.op (add_opposite.unop a / add_opposite.unop b)}

source

@[simp]

theorem add_opposite.op_div {α : Type u} [has_div α] (a b : α) :

add_opposite.op (a / b) = add_opposite.op a / add_opposite.op b

source

@[simp]

theorem add_opposite.unop_div {α : Type u} [has_div α] (a b : α) :

add_opposite.unop (a / b) = add_opposite.unop a / add_opposite.unop b

mathlib documentation

Multiplicative opposite and algebraic operations on it #

Notation #

Tags #