mathlib docs: data.equiv.mul

theorem mul_equiv.coe_mk {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x * y) = f x * f y) :

⇑{to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_mul' := h₃} = f

source

@[simp]

theorem add_equiv.coe_mk {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x + y) = f x + f y) :

⇑{to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_add' := h₃} = f

source

@[simp]

theorem add_equiv.coe_symm_mk {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x + y) = f x + f y) :

⇑({to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_add' := h₃}.symm) = g

source

@[simp]

theorem mul_equiv.coe_symm_mk {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (f : M → N) (g : N → M) (h₁ : function.left_inverse g f) (h₂ : function.right_inverse g f) (h₃ : ∀ (x y : M), f (x * y) = f x * f y) :

⇑({to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_mul' := h₃}.symm) = g

source

def add_equiv.trans {M : Type u_3} {N : Type u_4} {P : Type u_5} [has_add M] [has_add N] [has_add P] :

M ≃+ N → N ≃+ P → M ≃+ P

Transitivity of addition-preserving isomorphisms

source

def mul_equiv.trans {M : Type u_3} {N : Type u_4} {P : Type u_5} [has_mul M] [has_mul N] [has_mul P] :

M ≃* N → N ≃* P → M ≃* P

Transitivity of multiplication-preserving isomorphisms

Equations

h1.trans h2 = {to_fun := (h1.to_equiv.trans h2.to_equiv).to_fun, inv_fun := (h1.to_equiv.trans h2.to_equiv).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem add_equiv.apply_symm_apply {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) (y : N) :

⇑e (⇑(e.symm) y) = y

source

@[simp]

theorem mul_equiv.apply_symm_apply {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) (y : N) :

⇑e (⇑(e.symm) y) = y

e.right_inv in canonical form

source

@[simp]

theorem add_equiv.symm_apply_apply {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] (e : M ≃+ N) (x : M) :

⇑(e.symm) (⇑e x) = x

source

@[simp]

theorem mul_equiv.symm_apply_apply {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] (e : M ≃* N) (x : M) :

⇑(e.symm) (⇑e x) = x

e.left_inv in canonical form

source

@[simp]

theorem add_equiv.refl_apply {M : Type u_3} [has_add M] (m : M) :

⇑(add_equiv.refl M) m = m

source

@[simp]

theorem mul_equiv.refl_apply {M : Type u_3} [has_mul M] (m : M) :

⇑(mul_equiv.refl M) m = m

source

@[simp]

theorem mul_equiv.trans_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [has_mul M] [has_mul N] [has_mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) :

⇑(e₁.trans e₂) m = ⇑e₂ (⇑e₁ m)

source

@[simp]

theorem add_equiv.trans_apply {M : Type u_3} {N : Type u_4} {P : Type u_5} [has_add M] [has_add N] [has_add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (m : M) :

⇑(e₁.trans e₂) m = ⇑e₂ (⇑e₁ m)

source

@[simp]

theorem add_equiv.map_zero {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (h : M ≃+ N) :

⇑h 0 = 0

source

@[simp]

theorem mul_equiv.map_one {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (h : M ≃* N) :

⇑h 1 = 1

a multiplicative equiv of monoids sends 1 to 1 (and is hence a monoid isomorphism)

source

@[simp]

theorem add_equiv.map_eq_zero_iff {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (h : M ≃+ N) {x : M} :

⇑h x = 0 ↔ x = 0

source

@[simp]

theorem mul_equiv.map_eq_one_iff {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (h : M ≃* N) {x : M} :

⇑h x = 1 ↔ x = 1

source

theorem add_equiv.map_ne_zero_iff {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (h : M ≃+ N) {x : M} :

⇑h x ≠ 0 ↔ x ≠ 0

source

theorem mul_equiv.map_ne_one_iff {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (h : M ≃* N) {x : M} :

⇑h x ≠ 1 ↔ x ≠ 1

source

def add_equiv.of_bijective {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (f : M →+ N) :

function.bijective ⇑f → M ≃+ N

A bijective add_monoid homomorphism is an isomorphism

source

def mul_equiv.of_bijective {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (f : M →* N) :

function.bijective ⇑f → M ≃* N

A bijective monoid homomorphism is an isomorphism

Equations

mul_equiv.of_bijective f hf = {to_fun := (equiv.of_bijective ⇑f hf).to_fun, inv_fun := (equiv.of_bijective ⇑f hf).inv_fun, left_inv := _, right_inv := _, map_mul' := _}

source

def mul_equiv.to_monoid_hom {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] :

M ≃* N → M →* N

Extract the forward direction of a multiplicative equivalence as a multiplication-preserving function.

Equations

h.to_monoid_hom = {to_fun := h.to_fun, map_one' := _, map_mul' := _}

source

def add_equiv.to_add_monoid_hom {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] :

M ≃+ N → M →+ N

Extract the forward direction of an additive equivalence as an addition-preserving function.

source

@[simp]

theorem add_equiv.to_add_monoid_hom_apply {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (e : M ≃+ N) (x : M) :

⇑(e.to_add_monoid_hom) x = ⇑e x

source

@[simp]

theorem mul_equiv.to_monoid_hom_apply {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (e : M ≃* N) (x : M) :

⇑(e.to_monoid_hom) x = ⇑e x

source

@[simp]

theorem add_equiv.map_neg {G : Type u_6} {H : Type u_7} [add_group G] [add_group H] (h : G ≃+ H) (x : G) :

⇑h (-x) = -⇑h x

source

@[simp]

theorem mul_equiv.map_inv {G : Type u_6} {H : Type u_7} [group G] [group H] (h : G ≃* H) (x : G) :

⇑h x⁻¹ = (⇑h x)⁻¹

A multiplicative equivalence of groups preserves inversion.

source

@[instance]

def add_equiv.is_add_monoid_hom {M : Type u_1} {N : Type u_2} [add_monoid M] [add_monoid N] (h : M ≃+ N) :

is_add_monoid_hom ⇑h

source

@[instance]

def mul_equiv.is_monoid_hom {M : Type u_1} {N : Type u_2} [monoid M] [monoid N] (h : M ≃* N) :

is_monoid_hom ⇑h

A multiplicative bijection between two monoids is a monoid hom (deprecated -- use to_monoid_hom).

Equations

_ = _

source

@[instance]

def add_equiv.is_add_group_hom {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (h : G ≃+ H) :

is_add_group_hom ⇑h

source

@[instance]

def mul_equiv.is_group_hom {G : Type u_1} {H : Type u_2} [group G] [group H] (h : G ≃* H) :

is_group_hom ⇑h

A multiplicative bijection between two groups is a group hom (deprecated -- use to_monoid_hom).

Equations

_ = is_group_hom.mk

source

@[ext]

theorem add_equiv.ext {M : Type u_3} {N : Type u_4} [has_add M] [has_add N] {f g : M ≃+ N} :

(∀ (x : M), ⇑f x = ⇑g x) → f = g

Two additive isomorphisms agree if they are defined by the same underlying function.

source

@[ext]

theorem mul_equiv.ext {M : Type u_3} {N : Type u_4} [has_mul M] [has_mul N] {f g : M ≃* N} :

(∀ (x : M), ⇑f x = ⇑g x) → f = g

Two multiplicative isomorphisms agree if they are defined by the same underlying function.

source

theorem add_equiv.map_sub {A : Type u_1} {B : Type u_2} [add_group A] [add_group B] (h : A ≃+ B) (x y : A) :

⇑h (x - y) = ⇑h x - ⇑h y

An additive equivalence of additive groups preserves subtraction.

source

@[instance]

def add_equiv.inhabited {M : Type u_1} [has_add M] :

inhabited (M ≃+ M)

Equations

add_equiv.inhabited = {default := add_equiv.refl M _inst_1}

source

def mul_aut (M : Type u_1) [has_mul M] :

Type u_1

The group of multiplicative automorphisms.

Equations

mul_aut M = (M ≃* M)

source

def add_aut (M : Type u_1) [has_add M] :

Type u_1

The group of additive automorphisms.

source

@[instance]

def mul_aut.group (M : Type u_3) [has_mul M] :

group (mul_aut M)

The group operation on multiplicative automorphisms is defined by λ g h, mul_equiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x).

Equations

mul_aut.group M = {mul := λ (g h : M ≃* M), h.trans g, mul_assoc := _, one := mul_equiv.refl M _inst_1, one_mul := _, mul_one := _, inv := mul_equiv.symm _inst_1, mul_left_inv := _}

source

@[instance]

def mul_aut.inhabited (M : Type u_3) [has_mul M] :

inhabited (mul_aut M)

Equations

mul_aut.inhabited M = {default := 1}

source

@[simp]

theorem mul_aut.coe_mul (M : Type u_3) [has_mul M] (e₁ e₂ : mul_aut M) :

⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂

source

@[simp]

theorem mul_aut.coe_one (M : Type u_3) [has_mul M] :

⇑1 = id

source

theorem mul_aut.mul_def (M : Type u_3) [has_mul M] (e₁ e₂ : mul_aut M) :

e₁ * e₂ = mul_equiv.trans e₂ e₁

source

theorem mul_aut.one_def (M : Type u_3) [has_mul M] :

1 = mul_equiv.refl M

source

theorem mul_aut.inv_def (M : Type u_3) [has_mul M] (e₁ : mul_aut M) :

e₁⁻¹ = mul_equiv.symm e₁

source

@[simp]

theorem mul_aut.mul_apply (M : Type u_3) [has_mul M] (e₁ e₂ : mul_aut M) (m : M) :

⇑(e₁ * e₂) m = ⇑e₁ (⇑e₂ m)

source

@[simp]

theorem mul_aut.one_apply (M : Type u_3) [has_mul M] (m : M) :

⇑1 m = m

source

@[simp]

theorem mul_aut.apply_inv_self (M : Type u_3) [has_mul M] (e : mul_aut M) (m : M) :

⇑e (⇑e⁻¹ m) = m

source

@[simp]

theorem mul_aut.inv_apply_self (M : Type u_3) [has_mul M] (e : mul_aut M) (m : M) :

⇑e⁻¹ (⇑e m) = m

source

def mul_aut.to_perm (M : Type u_3) [has_mul M] :

mul_aut M →* equiv.perm M

Monoid hom from the group of multiplicative automorphisms to the group of permutations.

Equations

mul_aut.to_perm M = {to_fun := mul_equiv.to_equiv _inst_1, map_one' := _, map_mul' := _}

source

def mul_aut.conj {G : Type u_6} [group G] :

G →* mul_aut G

group conjugation as a group homomorphism into the automorphism group. conj g h = g * h * g⁻¹

Equations

mul_aut.conj = {to_fun := λ (g : G), {to_fun := λ (h : G), g * h * g⁻¹, inv_fun := λ (h : G), g⁻¹ * h * g, left_inv := _, right_inv := _, map_mul' := _}, map_one' := _, map_mul' := _}

source

@[simp]

theorem mul_aut.conj_apply {G : Type u_6} [group G] (g h : G) :

⇑(⇑mul_aut.conj g) h = g * h * g⁻¹

source

@[simp]

theorem mul_aut.conj_symm_apply {G : Type u_6} [group G] (g h : G) :

⇑(mul_equiv.symm (⇑mul_aut.conj g)) h = g⁻¹ * h * g

source

@[instance]

def add_aut.group (A : Type u_1) [has_add A] :

group (add_aut A)

The group operation on additive automorphisms is defined by λ g h, mul_equiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x).

Equations

add_aut.group A = {mul := λ (g h : A ≃+ A), h.trans g, mul_assoc := _, one := add_equiv.refl A _inst_1, one_mul := _, mul_one := _, inv := add_equiv.symm _inst_1, mul_left_inv := _}

source

@[instance]

def add_aut.inhabited (A : Type u_1) [has_add A] :

inhabited (add_aut A)

Equations

add_aut.inhabited A = {default := 1}

source

@[simp]

theorem add_aut.coe_mul (A : Type u_1) [has_add A] (e₁ e₂ : add_aut A) :

⇑(e₁ * e₂) = ⇑e₁ ∘ ⇑e₂

source

@[simp]

theorem add_aut.coe_one (A : Type u_1) [has_add A] :

⇑1 = id

source

theorem add_aut.mul_def (A : Type u_1) [has_add A] (e₁ e₂ : add_aut A) :

e₁ * e₂ = add_equiv.trans e₂ e₁

source

theorem add_aut.one_def (A : Type u_1) [has_add A] :

1 = add_equiv.refl A

source

theorem add_aut.inv_def (A : Type u_1) [has_add A] (e₁ : add_aut A) :

e₁⁻¹ = add_equiv.symm e₁

source

@[simp]

theorem add_aut.mul_apply (A : Type u_1) [has_add A] (e₁ e₂ : add_aut A) (a : A) :

⇑(e₁ * e₂) a = ⇑e₁ (⇑e₂ a)

source

@[simp]

theorem add_aut.one_apply (A : Type u_1) [has_add A] (a : A) :

⇑1 a = a

source

@[simp]

theorem add_aut.apply_inv_self (A : Type u_1) [has_add A] (e : add_aut A) (a : A) :

⇑e⁻¹ (⇑e a) = a

source

@[simp]

theorem add_aut.inv_apply_self (A : Type u_1) [has_add A] (e : add_aut A) (a : A) :

⇑e (⇑e⁻¹ a) = a

source

def add_aut.to_perm (A : Type u_1) [has_add A] :

add_aut A →* equiv.perm A

Monoid hom from the group of multiplicative automorphisms to the group of permutations.

Equations

add_aut.to_perm A = {to_fun := add_equiv.to_equiv _inst_1, map_one' := _, map_mul' := _}

source

def to_add_units {G : Type u_1} [add_group G] :

G ≃+ add_units G

An additive group is isomorphic to its group of additive units

source

def to_units {G : Type u_1} [group G] :

G ≃* units G

A group is isomorphic to its group of units.

Equations

to_units = {to_fun := λ (x : G), {val := x, inv := x⁻¹, val_inv := _, inv_val := _}, inv_fun := coe coe_to_lift, left_inv := _, right_inv := _, map_mul' := _}

source

def units.map_equiv {M : Type u_3} {N : Type u_4} [monoid M] [monoid N] :

M ≃* N → units M ≃* units N

A multiplicative equivalence of monoids defines a multiplicative equivalence of their groups of units.

Equations

units.map_equiv h = {to_fun := (units.map h.to_monoid_hom).to_fun, inv_fun := ⇑(units.map h.symm.to_monoid_hom), left_inv := _, right_inv := _, map_mul' := _}

source

def units.mul_left {M : Type u_3} [monoid M] :

units M → equiv.perm M

Left multiplication by a unit of a monoid is a permutation of the underlying type.

Equations

u.mul_left = {to_fun := λ (x : M), ↑u * x, inv_fun := λ (x : M), ↑u⁻¹ * x, left_inv := _, right_inv := _}

source

def add_units.add_left {M : Type u_3} [add_monoid M] :

add_units M → equiv.perm M

Left addition of an additive unit is a permutation of the underlying type.

source

@[simp]

theorem add_units.coe_add_left {M : Type u_3} [add_monoid M] (u : add_units M) :

⇑(u.add_left) = has_add.add ↑u

source

@[simp]

theorem units.coe_mul_left {M : Type u_3} [monoid M] (u : units M) :

⇑(u.mul_left) = has_mul.mul ↑u

source

@[simp]

theorem add_units.add_left_symm {M : Type u_3} [add_monoid M] (u : add_units M) :

equiv.symm u.add_left = (-u).add_left

source

@[simp]

theorem units.mul_left_symm {M : Type u_3} [monoid M] (u : units M) :

equiv.symm u.mul_left = u⁻¹.mul_left

source

def add_units.add_right {M : Type u_3} [add_monoid M] :

add_units M → equiv.perm M

Right addition of an additive unit is a permutation of the underlying type.

source

def units.mul_right {M : Type u_3} [monoid M] :

units M → equiv.perm M

Right multiplication by a unit of a monoid is a permutation of the underlying type.

Equations

u.mul_right = {to_fun := λ (x : M), x * ↑u, inv_fun := λ (x : M), x * ↑u⁻¹, left_inv := _, right_inv := _}

source

@[simp]

theorem add_units.coe_add_right {M : Type u_3} [add_monoid M] (u : add_units M) :

⇑(u.add_right) = λ (x : M), x + ↑u

source

@[simp]

theorem units.coe_mul_right {M : Type u_3} [monoid M] (u : units M) :

⇑(u.mul_right) = λ (x : M), x * ↑u

source

@[simp]

theorem add_units.add_right_symm {M : Type u_3} [add_monoid M] (u : add_units M) :

equiv.symm u.add_right = (-u).add_right

source

@[simp]

theorem units.mul_right_symm {M : Type u_3} [monoid M] (u : units M) :

equiv.symm u.mul_right = u⁻¹.mul_right

source

def equiv.add_left {G : Type u_6} [add_group G] :

G → equiv.perm G

Left addition in an add_group is a permutation of the underlying type.

source

def equiv.mul_left {G : Type u_6} [group G] :

G → equiv.perm G

Left multiplication in a group is a permutation of the underlying type.

Equations

equiv.mul_left a = (⇑to_units a).mul_left

source

@[simp]

theorem equiv.coe_mul_left {G : Type u_6} [group G] (a : G) :

⇑(equiv.mul_left a) = has_mul.mul a

source

@[simp]

theorem equiv.coe_add_left {G : Type u_6} [add_group G] (a : G) :

⇑(equiv.add_left a) = has_add.add a

source

@[simp]

theorem equiv.mul_left_symm {G : Type u_6} [group G] (a : G) :

equiv.symm (equiv.mul_left a) = equiv.mul_left a⁻¹

source

@[simp]

theorem equiv.add_left_symm {G : Type u_6} [add_group G] (a : G) :

equiv.symm (equiv.add_left a) = equiv.add_left (-a)

source

def equiv.mul_right {G : Type u_6} [group G] :

G → equiv.perm G

Right multiplication in a group is a permutation of the underlying type.

Equations

equiv.mul_right a = (⇑to_units a).mul_right

source

def equiv.add_right {G : Type u_6} [add_group G] :

G → equiv.perm G

Right addition in an add_group is a permutation of the underlying type.

source

@[simp]

theorem equiv.coe_add_right {G : Type u_6} [add_group G] (a : G) :

⇑(equiv.add_right a) = λ (x : G), x + a

source

@[simp]

theorem equiv.coe_mul_right {G : Type u_6} [group G] (a : G) :

⇑(equiv.mul_right a) = λ (x : G), x * a

source

@[simp]

theorem equiv.mul_right_symm {G : Type u_6} [group G] (a : G) :

equiv.symm (equiv.mul_right a) = equiv.mul_right a⁻¹

source

@[simp]

theorem equiv.add_right_symm {G : Type u_6} [add_group G] (a : G) :

equiv.symm (equiv.add_right a) = equiv.add_right (-a)

source

def equiv.inv (G : Type u_6) [group G] :

equiv.perm G

Inversion on a group is a permutation of the underlying type.

Equations

equiv.inv G = {to_fun := λ (a : G), a⁻¹, inv_fun := λ (a : G), a⁻¹, left_inv := _, right_inv := _}

source

def equiv.neg (G : Type u_6) [add_group G] :

equiv.perm G

Negation on an add_group is a permutation of the underlying type.

source

@[simp]

theorem equiv.coe_neg {G : Type u_6} [add_group G] :

⇑(equiv.neg G) = has_neg.neg

source

@[simp]

theorem equiv.coe_inv {G : Type u_6} [group G] :

⇑(equiv.inv G) = has_inv.inv

source

@[simp]

theorem equiv.neg_symm {G : Type u_6} [add_group G] :

equiv.symm (equiv.neg G) = equiv.neg G

source

@[simp]

theorem equiv.inv_symm {G : Type u_6} [group G] :

equiv.symm (equiv.inv G) = equiv.inv G

source

def equiv.point_reflection {A : Type u_1} [add_comm_group A] :

A → equiv.perm A

Point reflection in x as a permutation.

Equations

equiv.point_reflection x = equiv.trans (equiv.neg A) (equiv.add_left (x + x))

source

theorem equiv.point_reflection_apply {A : Type u_1} [add_comm_group A] (x y : A) :

⇑(equiv.point_reflection x) y = x + x - y

source

@[simp]

theorem equiv.point_reflection_self {A : Type u_1} [add_comm_group A] (x : A) :

⇑(equiv.point_reflection x) x = x

source

theorem equiv.point_reflection_involutive {A : Type u_1} [add_comm_group A] (x : A) :

function.involutive ⇑(equiv.point_reflection x)

source

@[simp]

theorem equiv.point_reflection_symm {A : Type u_1} [add_comm_group A] (x : A) :

equiv.symm (equiv.point_reflection x) = equiv.point_reflection x

source

theorem equiv.point_reflection_fixed_iff_of_bit0_injective {A : Type u_1} [add_comm_group A] {x y : A} :

function.injective bit0 → (⇑(equiv.point_reflection x) y = y ↔ y = x)

x is the only fixed point of point_reflection x. This lemma requires x + x = y + y ↔ x = y. There is no typeclass to use here, so we add it as an explicit argument.

source