mathlib docs: algebra.group.type

source

def additive :

Type u_1 → Type u_1

If α carries some multiplicative structure, then additive α carries the corresponding additive structure.

Equations

additive α = α

source

def multiplicative :

Type u_1 → Type u_1

If α carries some additive structure, then multiplicative α carries the corresponding multiplicative structure.

Equations

multiplicative α = α

source

def additive.of_mul {α : Type u} :

α → additive α

Reinterpret x : α as an element of additive α.

Equations

additive.of_mul x = x

source

def additive.to_mul {α : Type u} :

additive α → α

Reinterpret x : additive α as an element of α.

Equations

x.to_mul = x

source

theorem of_mul_injective {α : Type u} :

function.injective additive.of_mul

source

theorem to_mul_injective {α : Type u} :

function.injective additive.to_mul

source

def multiplicative.of_add {α : Type u} :

α → multiplicative α

Reinterpret x : α as an element of multiplicative α.

Equations

multiplicative.of_add x = x

source

def multiplicative.to_add {α : Type u} :

multiplicative α → α

Reinterpret x : multiplicative α as an element of α.

Equations

x.to_add = x

source

theorem of_add_injective {α : Type u} :

function.injective multiplicative.of_add

source

theorem to_add_injective {α : Type u} :

function.injective multiplicative.to_add

source

@[simp]

theorem to_add_of_add {α : Type u} (x : α) :

(multiplicative.of_add x).to_add = x

source

@[simp]

theorem of_add_to_add {α : Type u} (x : multiplicative α) :

multiplicative.of_add x.to_add = x

source

@[simp]

theorem to_mul_of_mul {α : Type u} (x : α) :

(additive.of_mul x).to_mul = x

source

@[simp]

theorem of_mul_to_mul {α : Type u} (x : additive α) :

additive.of_mul x.to_mul = x

source

@[instance]

def additive.inhabited {α : Type u} [inhabited α] :

inhabited (additive α)

Equations

additive.inhabited = {default := additive.of_mul (inhabited.default α)}

source

@[instance]

def multiplicative.inhabited {α : Type u} [inhabited α] :

inhabited (multiplicative α)

Equations

multiplicative.inhabited = {default := multiplicative.of_add (inhabited.default α)}

source

@[instance]

def additive.has_add {α : Type u} [has_mul α] :

has_add (additive α)

Equations

additive.has_add = {add := λ (x y : additive α), additive.of_mul (x.to_mul * y.to_mul)}

source

@[instance]

def multiplicative.has_mul {α : Type u} [has_add α] :

has_mul (multiplicative α)

Equations

multiplicative.has_mul = {mul := λ (x y : multiplicative α), multiplicative.of_add (x.to_add + y.to_add)}

source

@[simp]

theorem of_add_add {α : Type u} [has_add α] (x y : α) :

multiplicative.of_add (x + y) = multiplicative.of_add x * multiplicative.of_add y

source

@[simp]

theorem to_add_mul {α : Type u} [has_add α] (x y : multiplicative α) :

(x * y).to_add = x.to_add + y.to_add

source

@[simp]

theorem of_mul_mul {α : Type u} [has_mul α] (x y : α) :

additive.of_mul (x * y) = additive.of_mul x + additive.of_mul y

source

@[simp]

theorem to_mul_add {α : Type u} [has_mul α] (x y : additive α) :

(x + y).to_mul = x.to_mul * y.to_mul

source

@[instance]

def additive.add_semigroup {α : Type u} [semigroup α] :

add_semigroup (additive α)

Equations

additive.add_semigroup = {add := has_add.add additive.has_add, add_assoc := _}

source

@[instance]

def multiplicative.semigroup {α : Type u} [add_semigroup α] :

semigroup (multiplicative α)

Equations

multiplicative.semigroup = {mul := has_mul.mul multiplicative.has_mul, mul_assoc := _}

source

@[instance]

def additive.add_comm_semigroup {α : Type u} [comm_semigroup α] :

add_comm_semigroup (additive α)

Equations

additive.add_comm_semigroup = {add := add_semigroup.add additive.add_semigroup, add_assoc := _, add_comm := _}

source

@[instance]

def multiplicative.comm_semigroup {α : Type u} [add_comm_semigroup α] :

comm_semigroup (multiplicative α)

Equations

multiplicative.comm_semigroup = {mul := semigroup.mul multiplicative.semigroup, mul_assoc := _, mul_comm := _}

source

@[instance]

def additive.add_left_cancel_semigroup {α : Type u} [left_cancel_semigroup α] :

add_left_cancel_semigroup (additive α)

Equations

additive.add_left_cancel_semigroup = {add := add_semigroup.add additive.add_semigroup, add_assoc := _, add_left_cancel := _}

source

@[instance]

def multiplicative.left_cancel_semigroup {α : Type u} [add_left_cancel_semigroup α] :

left_cancel_semigroup (multiplicative α)

Equations

multiplicative.left_cancel_semigroup = {mul := semigroup.mul multiplicative.semigroup, mul_assoc := _, mul_left_cancel := _}

source

@[instance]

def additive.add_right_cancel_semigroup {α : Type u} [right_cancel_semigroup α] :

add_right_cancel_semigroup (additive α)

Equations

additive.add_right_cancel_semigroup = {add := add_semigroup.add additive.add_semigroup, add_assoc := _, add_right_cancel := _}

source

@[instance]

def multiplicative.right_cancel_semigroup {α : Type u} [add_right_cancel_semigroup α] :

right_cancel_semigroup (multiplicative α)

Equations

multiplicative.right_cancel_semigroup = {mul := semigroup.mul multiplicative.semigroup, mul_assoc := _, mul_right_cancel := _}

source

@[instance]

def additive.has_zero {α : Type u} [has_one α] :

has_zero (additive α)

Equations

additive.has_zero = {zero := additive.of_mul 1}

source

@[simp]

theorem of_mul_one {α : Type u} [has_one α] :

additive.of_mul 1 = 0

source

@[simp]

theorem to_mul_zero {α : Type u} [has_one α] :

0.to_mul = 1

source

@[instance]

def multiplicative.has_one {α : Type u} [has_zero α] :

has_one (multiplicative α)

Equations

multiplicative.has_one = {one := multiplicative.of_add 0}

source

@[simp]

theorem of_add_zero {α : Type u} [has_zero α] :

multiplicative.of_add 0 = 1

source

@[simp]

theorem to_add_one {α : Type u} [has_zero α] :

1.to_add = 0

source

@[instance]

def additive.add_monoid {α : Type u} [monoid α] :

add_monoid (additive α)

Equations

additive.add_monoid = {add := add_semigroup.add additive.add_semigroup, add_assoc := _, zero := 0, zero_add := _, add_zero := _}

source

@[instance]

def multiplicative.monoid {α : Type u} [add_monoid α] :

monoid (multiplicative α)

Equations

multiplicative.monoid = {mul := semigroup.mul multiplicative.semigroup, mul_assoc := _, one := 1, one_mul := _, mul_one := _}

source

@[instance]

def additive.add_comm_monoid {α : Type u} [comm_monoid α] :

add_comm_monoid (additive α)

Equations

additive.add_comm_monoid = {add := add_monoid.add additive.add_monoid, add_assoc := _, zero := add_monoid.zero additive.add_monoid, zero_add := _, add_zero := _, add_comm := _}

source

@[instance]

def multiplicative.comm_monoid {α : Type u} [add_comm_monoid α] :

comm_monoid (multiplicative α)

Equations

multiplicative.comm_monoid = {mul := monoid.mul multiplicative.monoid, mul_assoc := _, one := monoid.one multiplicative.monoid, one_mul := _, mul_one := _, mul_comm := _}

source

@[instance]

def additive.has_neg {α : Type u} [has_inv α] :

has_neg (additive α)

Equations

additive.has_neg = {neg := λ (x : additive α), multiplicative.of_add (x.to_mul)⁻¹}

source

@[simp]

theorem of_mul_inv {α : Type u} [has_inv α] (x : α) :

additive.of_mul x⁻¹ = -additive.of_mul x

source

@[simp]

theorem to_mul_neg {α : Type u} [has_inv α] (x : additive α) :

(-x).to_mul = (x.to_mul)⁻¹

source

@[instance]

def multiplicative.has_inv {α : Type u} [has_neg α] :

has_inv (multiplicative α)

Equations

multiplicative.has_inv = {inv := λ (x : multiplicative α), additive.of_mul (-x.to_add)}

source

@[simp]

theorem of_add_neg {α : Type u} [has_neg α] (x : α) :

multiplicative.of_add (-x) = (multiplicative.of_add x)⁻¹

source

@[simp]

theorem to_add_inv {α : Type u} [has_neg α] (x : multiplicative α) :

x⁻¹.to_add = -x.to_add

source

@[instance]

def additive.add_group {α : Type u} [group α] :

add_group (additive α)

Equations

additive.add_group = {add := add_monoid.add additive.add_monoid, add_assoc := _, zero := add_monoid.zero additive.add_monoid, zero_add := _, add_zero := _, neg := has_neg.neg additive.has_neg, add_left_neg := _}

source

@[instance]

def multiplicative.group {α : Type u} [add_group α] :

group (multiplicative α)

Equations

multiplicative.group = {mul := monoid.mul multiplicative.monoid, mul_assoc := _, one := monoid.one multiplicative.monoid, one_mul := _, mul_one := _, inv := has_inv.inv multiplicative.has_inv, mul_left_inv := _}

source

@[instance]

def additive.add_comm_group {α : Type u} [comm_group α] :

add_comm_group (additive α)

Equations

additive.add_comm_group = {add := add_group.add additive.add_group, add_assoc := _, zero := add_group.zero additive.add_group, zero_add := _, add_zero := _, neg := add_group.neg additive.add_group, add_left_neg := _, add_comm := _}

source

@[instance]

def multiplicative.comm_group {α : Type u} [add_comm_group α] :

comm_group (multiplicative α)

Equations

multiplicative.comm_group = {mul := group.mul multiplicative.group, mul_assoc := _, one := group.one multiplicative.group, one_mul := _, mul_one := _, inv := group.inv multiplicative.group, mul_left_inv := _, mul_comm := _}

source

def add_monoid_hom.to_multiplicative {α : Type u} {β : Type v} [add_monoid α] [add_monoid β] :

(α →+ β) → multiplicative α →* multiplicative β

Reinterpret f : α →+ β as multiplicative α →* multiplicative β.

Equations

f.to_multiplicative = {to_fun := f.to_fun, map_one' := _, map_mul' := _}

source

def monoid_hom.to_additive {α : Type u} {β : Type v} [monoid α] [monoid β] :

(α →* β) → additive α →+ additive β

Reinterpret f : α →* β as additive α →+ additive β.

Equations

f.to_additive = {to_fun := f.to_fun, map_zero' := _, map_add' := _}

source

def add_monoid_hom.to_multiplicative' {α : Type u} {β : Type v} [monoid α] [add_monoid β] :

(additive α →+ β) → α →* multiplicative β

Reinterpret f : additive α →+ β as α →* multiplicative β.

Equations

f.to_multiplicative' = {to_fun := f.to_fun, map_one' := _, map_mul' := _}

source

def monoid_hom.to_additive' {α : Type u} {β : Type v} [monoid α] [add_monoid β] :

(α →* multiplicative β) → additive α →+ β

Reinterpret f : α →* multiplicative β as additive α →+ β.

Equations

f.to_additive' = {to_fun := f.to_fun, map_zero' := _, map_add' := _}

mathlib documentation

algebra.group.type_tags

Type tags that turn additive structures into multiplicative, and vice versa

General documentation

Additional documentation

Library

mathlib documentation

algebra.​group.​type_tags

Type tags that turn additive structures into multiplicative, and vice versa

General documentation

Additional documentation

Library

algebra.group.type_tags