# Multiplicative and additive equivs #

In this file we define two extensions of `Equiv` called `AddEquiv` and `MulEquiv`, which are datatypes representing isomorphisms of `AddMonoid`s/`AddGroup`s and `Monoid`s/`Group`s.

## Main definitions #

- `≃*` (`MulEquiv`), `≃+` (`AddEquiv`): bundled equivalences that preserve multiplication/addition (and are therefore monoid and group isomorphisms).
- `MulEquivClass`, `AddEquivClass`: classes for types containing bundled equivalences that preserve multiplication/addition.

## Notation #

- `infix ` ≃* `:25 := MulEquiv`
- `infix ` ≃+ `:25 := AddEquiv`

The extended equivs all have coercions to functions, and the coercions are the canonical notation when treating the isomorphisms as maps.

## Tags #

Equiv, MulEquiv, AddEquiv

source
@[simp]
theorem EmbeddingLike.map_eq_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} :
f x = 1 ↔ x = 1
source
@[simp]
theorem EmbeddingLike.map_eq_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} :
f x = 0 ↔ x = 0
source
theorem EmbeddingLike.map_ne_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} :
f x ≠ 1 ↔ x ≠ 1
source
theorem EmbeddingLike.map_ne_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} :
f x ≠ 0 ↔ x ≠ 0
source
structure AddEquiv (A : Type u_9) (B : Type u_10) [Add A] [Add B] extends A ≃ B, A →ₙ+ B :
Type (max u_10 u_9)

`AddEquiv α β` is the type of an equiv `α ≃ β` which preserves addition.

- toFun : A → B
- invFun : B → A
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- map_add' (x y : A) : self.toFun (x + y) = self.toFun x + self.toFun y

Instances For

source
class AddEquivClass (F : Type u_9) (A : outParam (Type u_10)) (B : outParam (Type u_11)) [Add A] [Add B] [EquivLike F A B] :
Prop

`AddEquivClass F A B` states that `F` is a type of addition-preserving morphisms. You should extend this class when you extend `AddEquiv`.

- map_add (f : F) (a b : A) : f (a + b) = f a + f b

  Preserves addition.

Instances

source
structure MulEquiv (M : Type u_9) (N : Type u_10) [Mul M] [Mul N] extends M ≃ N, M →ₙ* N :
Type (max u_10 u_9)

`MulEquiv α β` is the type of an equiv `α ≃ β` which preserves multiplication.

- toFun : M → N
- invFun : N → M
- left_inv : Function.LeftInverse self.invFun self.toFun
- right_inv : Function.RightInverse self.invFun self.toFun
- map_mul' (x y : M) : self.toFun (x * y) = self.toFun x * self.toFun y

Instances For

source
def «term_≃*_» :
Lean.TrailingParserDescr

Notation for a `MulEquiv`.

Equations

- «term_≃*_» = Lean.ParserDescr.trailingNode `«term_≃*_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃* ") (Lean.ParserDescr.cat `term 26))

Instances For

source
def «term_≃+_» :
Lean.TrailingParserDescr

Notation for an `AddEquiv`.

Equations

- «term_≃+_» = Lean.ParserDescr.trailingNode `«term_≃+_» 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃+ ") (Lean.ParserDescr.cat `term 26))

Instances For

source
theorem MulEquiv.toEquiv_injective {α : Type u_9} {β : Type u_10} [Mul α] [Mul β] :
Function.Injective toEquiv
source
theorem AddEquiv.toEquiv_injective {α : Type u_9} {β : Type u_10} [Add α] [Add β] :
Function.Injective toEquiv
source
class MulEquivClass (F : Type u_9) (A : outParam (Type u_10)) (B : outParam (Type u_11)) [Mul A] [Mul B] [EquivLike F A B] :
Prop

`MulEquivClass F A B` states that `F` is a type of multiplication-preserving morphisms. You should extend this class when you extend `MulEquiv`.

- map_mul (f : F) (a b : A) : f (a * b) = f a * f b

  Preserves multiplication.

Instances

source
theorem MulEquivClass.map_eq_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} :
f x = 1 ↔ x = 1

Alias of `EmbeddingLike.map_eq_one_iff`.

source
theorem AddEquivClass.map_eq_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} :
f x = 0 ↔ x = 0
source
theorem MulEquivClass.map_ne_one_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [One M] [One N] [FunLike F M N] [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M} :
f x ≠ 1 ↔ x ≠ 1

Alias of `EmbeddingLike.map_ne_one_iff`.

source
theorem AddEquivClass.map_ne_zero_iff {F : Type u_1} {M : Type u_4} {N : Type u_5} [Zero M] [Zero N] [FunLike F M N] [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M} :
f x ≠ 0 ↔ x ≠ 0
source
@[instance 100]
instance MulEquivClass.instMulHomClass {M : Type u_4} {N : Type u_5} (F : Type u_9) [Mul M] [Mul N] [EquivLike F M N] [h : MulEquivClass F M N] :
MulHomClass F M N
source
@[instance 100]
instance AddEquivClass.instAddHomClass {M : Type u_4} {N : Type u_5} (F : Type u_9) [Add M] [Add N] [EquivLike F M N] [h : AddEquivClass F M N] :
AddHomClass F M N
source
@[instance 100]
instance MulEquivClass.instMonoidHomClass (F : Type u_1) {M : Type u_4} {N : Type u_5} [EquivLike F M N] [MulOneClass M] [MulOneClass N] [MulEquivClass F M N] :
MonoidHomClass F M N
source
@[instance 100]
instance AddEquivClass.instAddMonoidHomClass (F : Type u_1) {M : Type u_4} {N : Type u_5} [EquivLike F M N] [AddZeroClass M] [AddZeroClass N] [AddEquivClass F M N] :
AddMonoidHomClass F M N
source
def MulEquivClass.toMulEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [MulEquivClass F α β] (f : F) :
α ≃* β

Turn an element of a type `F` satisfying `MulEquivClass F α β` into an actual `MulEquiv`. This is declared as the default coercion from `F` to `α ≃* β`.

Equations

- ↑f = { toEquiv := ↑f, map_mul' := ⋯ }

Instances For

source
def AddEquivClass.toAddEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] (f : F) :
α ≃+ β

Turn an element of a type `F` satisfying `AddEquivClass F α β` into an actual `AddEquiv`. This is declared as the default coercion from `F` to `α ≃+ β`.

Equations

- ↑f = { toEquiv := ↑f, map_add' := ⋯ }

Instances For

source
instance instCoeTCMulEquivOfMulEquivClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Mul α] [Mul β] [MulEquivClass F α β] :
CoeTC F (α ≃* β)

Any type satisfying `MulEquivClass` can be cast into `MulEquiv` via `MulEquivClass.toMulEquiv`.

Equations

- instCoeTCMulEquivOfMulEquivClass = { coe := MulEquivClass.toMulEquiv }

source
instance instCoeTCAddEquivOfAddEquivClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [EquivLike F α β] [Add α] [Add β] [AddEquivClass F α β] :
CoeTC F (α ≃+ β)

Any type satisfying `AddEquivClass` can be cast into `AddEquiv` via `AddEquivClass.toAddEquiv`.

Equations

- instCoeTCAddEquivOfAddEquivClass = { coe := AddEquivClass.toAddEquiv }

source
instance MulEquiv.instEquivLike {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :
EquivLike (M ≃* N) M N
Equations

- MulEquiv.instEquivLike = { coe := fun (f : M ≃* N) => f.toFun, inv := fun (f : M ≃* N) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

source
instance AddEquiv.instEquivLike {M : Type u_4} {N : Type u_5} [Add M] [Add N] :
EquivLike (M ≃+ N) M N
Equations

- AddEquiv.instEquivLike = { coe := fun (f : M ≃+ N) => f.toFun, inv := fun (f : M ≃+ N) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }

source
instance MulEquiv.instCoeFunForall {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :
CoeFun (M ≃* N) fun (x : M ≃* N) => M → N
Equations

- MulEquiv.instCoeFunForall = { coe := fun (f : M ≃* N) => ⇑f }

source
instance AddEquiv.instCoeFunForall {M : Type u_4} {N : Type u_5} [Add M] [Add N] :
CoeFun (M ≃+ N) fun (x : M ≃+ N) => M → N
Equations

- AddEquiv.instCoeFunForall = { coe := fun (f : M ≃+ N) => ⇑f }

source
instance MulEquiv.instMulEquivClass {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :
MulEquivClass (M ≃* N) M N
source
instance AddEquiv.instAddEquivClass {M : Type u_4} {N : Type u_5} [Add M] [Add N] :
AddEquivClass (M ≃+ N) M N
source
theorem MulEquiv.ext {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f g : M ≃* N} (h : ∀ (x : M), f x = g x) :
f = g

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

source
theorem AddEquiv.ext {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f g : M ≃+ N} (h : ∀ (x : M), f x = g x) :
f = g

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

source
theorem MulEquiv.ext_iff {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f g : M ≃* N} :
f = g ↔ ∀ (x : M), f x = g x
source
theorem AddEquiv.ext_iff {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f g : M ≃+ N} :
f = g ↔ ∀ (x : M), f x = g x
source
theorem MulEquiv.congr_arg {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f : M ≃* N} {x x' : M} :
x = x' → f x = f x'
source
theorem AddEquiv.congr_arg {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f : M ≃+ N} {x x' : M} :
x = x' → f x = f x'
source
theorem MulEquiv.congr_fun {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f g : M ≃* N} (h : f = g) (x : M) :
f x = g x
source
theorem AddEquiv.congr_fun {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f g : M ≃+ N} (h : f = g) (x : M) :
f x = g x
source
@[simp]
theorem MulEquiv.coe_mk {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃ N) (hf : ∀ (x y : M), f (x * y) = f x * f y) :
⇑{ toEquiv := f, map_mul' := hf } = ⇑f
source
@[simp]
theorem AddEquiv.coe_mk {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃ N) (hf : ∀ (x y : M), f (x + y) = f x + f y) :
⇑{ toEquiv := f, map_add' := hf } = ⇑f
source
@[simp]
theorem MulEquiv.mk_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) (e' : N → M) (h₁ : Function.LeftInverse e' ⇑e) (h₂ : Function.RightInverse e' ⇑e) (h₃ : ∀ (x y : M), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y) :
{ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃ } = e
source
@[simp]
theorem AddEquiv.mk_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) (e' : N → M) (h₁ : Function.LeftInverse e' ⇑e) (h₂ : Function.RightInverse e' ⇑e) (h₃ : ∀ (x y : M), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y) :
{ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_add' := h₃ } = e
source
@[simp]
theorem MulEquiv.toEquiv_eq_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
f.toEquiv = ↑f
source
@[simp]
theorem AddEquiv.toEquiv_eq_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
f.toEquiv = ↑f
source
@[simp]
theorem MulEquiv.toMulHom_eq_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
f.toMulHom = ↑f

The `simp`-normal form to turn something into a `MulHom` is via `MulHomClass.toMulHom`.

source
@[simp]
theorem AddEquiv.toAddHom_eq_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
f.toAddHom = ↑f
source
theorem MulEquiv.toFun_eq_coe {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
f.toFun = ⇑f
source
theorem AddEquiv.toFun_eq_coe {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
f.toFun = ⇑f
source
@[simp]
theorem MulEquiv.coe_toEquiv {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
⇑↑f = ⇑f

`simp`-normal form of `toFun_eq_coe`.

source
@[simp]
theorem AddEquiv.coe_toEquiv {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
⇑↑f = ⇑f
source
@[simp]
theorem MulEquiv.coe_toMulHom {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f : M ≃* N} :
⇑f.toMulHom = ⇑f
source
@[simp]
theorem AddEquiv.coe_toAddHom {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f : M ≃+ N} :
⇑f.toAddHom = ⇑f
source
def MulEquiv.mk' {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃ N) (h : ∀ (x y : M), f (x * y) = f x * f y) :
M ≃* N

Makes a multiplicative isomorphism from a bijection which preserves multiplication.

Equations

- MulEquiv.mk' f h = { toEquiv := f, map_mul' := h }

Instances For

source
def AddEquiv.mk' {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃ N) (h : ∀ (x y : M), f (x + y) = f x + f y) :
M ≃+ N

Makes an additive isomorphism from a bijection which preserves addition.

Equations

- AddEquiv.mk' f h = { toEquiv := f, map_add' := h }

Instances For

source
theorem MulEquiv.map_mul {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) (x y : M) :
f (x * y) = f x * f y

A multiplicative isomorphism preserves multiplication.

source
theorem AddEquiv.map_add {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) (x y : M) :
f (x + y) = f x + f y

An additive isomorphism preserves addition.

source
theorem MulEquiv.bijective {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
Function.Bijective ⇑e
source
theorem AddEquiv.bijective {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
Function.Bijective ⇑e
source
theorem MulEquiv.injective {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
Function.Injective ⇑e
source
theorem AddEquiv.injective {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
Function.Injective ⇑e
source
theorem MulEquiv.surjective {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
Function.Surjective ⇑e
source
theorem AddEquiv.surjective {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
Function.Surjective ⇑e
source
theorem MulEquiv.apply_eq_iff_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x y : M} :
e x = e y ↔ x = y
source
theorem AddEquiv.apply_eq_iff_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x y : M} :
e x = e y ↔ x = y
source
def MulEquiv.refl (M : Type u_9) [Mul M] :
M ≃* M

The identity map is a multiplicative isomorphism.

Equations

- MulEquiv.refl M = { toEquiv := Equiv.refl M, map_mul' := ⋯ }

Instances For

source
def AddEquiv.refl (M : Type u_9) [Add M] :
M ≃+ M

The identity map is an additive isomorphism.

Equations

- AddEquiv.refl M = { toEquiv := Equiv.refl M, map_add' := ⋯ }

Instances For

source
instance MulEquiv.instInhabited {M : Type u_4} [Mul M] :
Inhabited (M ≃* M)
Equations

- MulEquiv.instInhabited = { default := MulEquiv.refl M }

source
instance AddEquiv.instInhabited {M : Type u_4} [Add M] :
Inhabited (M ≃+ M)
Equations

- AddEquiv.instInhabited = { default := AddEquiv.refl M }

source
@[simp]
theorem MulEquiv.coe_refl {M : Type u_4} [Mul M] :
⇑(refl M) = id
source
@[simp]
theorem AddEquiv.coe_refl {M : Type u_4} [Add M] :
⇑(refl M) = id
source
@[simp]
theorem MulEquiv.refl_apply {M : Type u_4} [Mul M] (m : M) :
(refl M) m = m
source
@[simp]
theorem AddEquiv.refl_apply {M : Type u_4} [Add M] (m : M) :
(refl M) m = m
source
theorem MulEquiv.symm_map_mul {M : Type u_9} {N : Type u_10} [Mul M] [Mul N] (h : M ≃* N) (x y : N) :
h.symm (x * y) = h.symm x * h.symm y

An alias for `h.symm.map_mul`. Introduced to fix the issue in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.234183.20.60simps.60.20maximum.20recursion.20depth

source
theorem AddEquiv.symm_map_add {M : Type u_9} {N : Type u_10} [Add M] [Add N] (h : M ≃+ N) (x y : N) :
h.symm (x + y) = h.symm x + h.symm y
source
def MulEquiv.symm {M : Type u_9} {N : Type u_10} [Mul M] [Mul N] (h : M ≃* N) :
N ≃* M

The inverse of an isomorphism is an isomorphism.

Equations

- h.symm = { toEquiv := h.symm, map_mul' := ⋯ }

Instances For

source
def AddEquiv.symm {M : Type u_9} {N : Type u_10} [Add M] [Add N] (h : M ≃+ N) :
N ≃+ M

The inverse of an isomorphism is an isomorphism.

Equations

- h.symm = { toEquiv := h.symm, map_add' := ⋯ }

Instances For

source
theorem MulEquiv.invFun_eq_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {f : M ≃* N} :
f.invFun = ⇑f.symm
source
theorem AddEquiv.invFun_eq_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] {f : M ≃+ N} :
f.invFun = ⇑f.symm
source
@[simp]
theorem MulEquiv.coe_toEquiv_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
⇑(↑f).symm = ⇑f.symm

`simp`-normal form of `invFun_eq_symm`.

source
@[simp]
theorem AddEquiv.coe_toEquiv_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
⇑(↑f).symm = ⇑f.symm
source
@[simp]
theorem MulEquiv.equivLike_inv_eq_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
EquivLike.inv f = ⇑f.symm
source
@[simp]
theorem AddEquiv.equivLike_neg_eq_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
EquivLike.inv f = ⇑f.symm
source
@[simp]
theorem MulEquiv.toEquiv_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
↑f.symm = (↑f).symm
source
@[simp]
theorem AddEquiv.toEquiv_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
↑f.symm = (↑f).symm
source
@[simp]
theorem MulEquiv.symm_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃* N) :
f.symm.symm = f
source
@[simp]
theorem AddEquiv.symm_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃+ N) :
f.symm.symm = f
source
theorem MulEquiv.symm_bijective {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] :
Function.Bijective symm
source
theorem AddEquiv.symm_bijective {M : Type u_4} {N : Type u_5} [Add M] [Add N] :
Function.Bijective symm
source
@[simp]
theorem MulEquiv.mk_coe' {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) (f : N → M) (h₁ : Function.LeftInverse (⇑e) f) (h₂ : Function.RightInverse (⇑e) f) (h₃ : ∀ (x y : N), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y) :
{ toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃ } = e.symm
source
@[simp]
theorem AddEquiv.mk_coe' {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) (f : N → M) (h₁ : Function.LeftInverse (⇑e) f) (h₂ : Function.RightInverse (⇑e) f) (h₃ : ∀ (x y : N), { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y) :
{ toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_add' := h₃ } = e.symm
source
@[simp]
theorem MulEquiv.symm_mk {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M ≃ N) (h : ∀ (x y : M), f.toFun (x * y) = f.toFun x * f.toFun y) :
{ toEquiv := f, map_mul' := h }.symm = { toEquiv := f.symm, map_mul' := ⋯ }
source
@[simp]
theorem AddEquiv.symm_mk {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M ≃ N) (h : ∀ (x y : M), f.toFun (x + y) = f.toFun x + f.toFun y) :
{ toEquiv := f, map_add' := h }.symm = { toEquiv := f.symm, map_add' := ⋯ }
source
@[simp]
theorem MulEquiv.refl_symm {M : Type u_4} [Mul M] :
(refl M).symm = refl M
source
@[simp]
theorem AddEquiv.refl_symm {M : Type u_4} [Add M] :
(refl M).symm = refl M
source
@[simp]
theorem MulEquiv.apply_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) (y : N) :
e (e.symm y) = y

`e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`.

source
@[simp]
theorem AddEquiv.apply_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) (y : N) :
e (e.symm y) = y

`e.symm` is a right inverse of `e`, written as `e (e.symm y) = y`.

source
@[simp]
theorem MulEquiv.symm_apply_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) (x : M) :
e.symm (e x) = x

`e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`.

source
@[simp]
theorem AddEquiv.symm_apply_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) (x : M) :
e.symm (e x) = x

`e.symm` is a left inverse of `e`, written as `e.symm (e y) = y`.

source
@[simp]
theorem MulEquiv.symm_comp_self {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
⇑e.symm ∘ ⇑e = id
source
@[simp]
theorem AddEquiv.symm_comp_self {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
⇑e.symm ∘ ⇑e = id
source
@[simp]
theorem MulEquiv.self_comp_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
⇑e ∘ ⇑e.symm = id
source
@[simp]
theorem AddEquiv.self_comp_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
⇑e ∘ ⇑e.symm = id
source
theorem MulEquiv.apply_eq_iff_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x : M} {y : N} :
e x = y ↔ x = e.symm y
source
theorem AddEquiv.apply_eq_iff_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x : M} {y : N} :
e x = y ↔ x = e.symm y
source
theorem MulEquiv.symm_apply_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} :
e.symm x = y ↔ x = e y
source
theorem AddEquiv.symm_apply_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x : N} {y : M} :
e.symm x = y ↔ x = e y
source
theorem MulEquiv.eq_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) {x : N} {y : M} :
y = e.symm x ↔ e y = x
source
theorem AddEquiv.eq_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) {x : N} {y : M} :
y = e.symm x ↔ e y = x
source
theorem MulEquiv.eq_comp_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : N → α) (g : M → α) :
f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
source
theorem AddEquiv.eq_comp_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : N → α) (g : M → α) :
f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
source
theorem MulEquiv.comp_symm_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : N → α) (g : M → α) :
g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
source
theorem AddEquiv.comp_symm_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : N → α) (g : M → α) :
g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
source
theorem MulEquiv.eq_symm_comp {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : α → M) (g : α → N) :
f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
source
theorem AddEquiv.eq_symm_comp {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : α → M) (g : α → N) :
f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
source
theorem MulEquiv.symm_comp_eq {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] {α : Type u_9} (e : M ≃* N) (f : α → M) (g : α → N) :
⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
source
theorem AddEquiv.symm_comp_eq {M : Type u_4} {N : Type u_5} [Add M] [Add N] {α : Type u_9} (e : M ≃+ N) (f : α → M) (g : α → N) :
⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
source
@[simp]
theorem MulEquivClass.apply_coe_symm_apply {α : Type u_9} {β : Type u_10} [Mul α] [Mul β] {F : Type u_11} [EquivLike F α β] [MulEquivClass F α β] (e : F) (x : β) :
e ((↑e).symm x) = x
source
@[simp]
theorem AddEquivClass.apply_coe_symm_apply {α : Type u_9} {β : Type u_10} [Add α] [Add β] {F : Type u_11} [EquivLike F α β] [AddEquivClass F α β] (e : F) (x : β) :
e ((↑e).symm x) = x
source
@[simp]
theorem MulEquivClass.coe_symm_apply_apply {α : Type u_9} {β : Type u_10} [Mul α] [Mul β] {F : Type u_11} [EquivLike F α β] [MulEquivClass F α β] (e : F) (x : α) :
(↑e).symm (e x) = x
source
@[simp]
theorem AddEquivClass.coe_symm_apply_apply {α : Type u_9} {β : Type u_10} [Add α] [Add β] {F : Type u_11} [EquivLike F α β] [AddEquivClass F α β] (e : F) (x : α) :
(↑e).symm (e x) = x
source
def MulEquiv.Simps.symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
N → M

See Note [custom simps projection]

Equations

- MulEquiv.Simps.symm_apply e = ⇑e.symm

Instances For

source
def AddEquiv.Simps.symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
N → M

See Note [custom simps projection]

Equations

- AddEquiv.Simps.symm_apply e = ⇑e.symm

Instances For

source
def MulEquiv.trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (h1 : M ≃* N) (h2 : N ≃* P) :
M ≃* P

Transitivity of multiplication-preserving isomorphisms

Equations

- h1.trans h2 = { toEquiv := h1.trans h2.toEquiv, map_mul' := ⋯ }

Instances For

source
def AddEquiv.trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (h1 : M ≃+ N) (h2 : N ≃+ P) :
M ≃+ P

Transitivity of addition-preserving isomorphisms

Equations

- h1.trans h2 = { toEquiv := h1.trans h2.toEquiv, map_add' := ⋯ }

Instances For

source
@[simp]
theorem MulEquiv.coe_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
source
@[simp]
theorem AddEquiv.coe_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
source
@[simp]
theorem MulEquiv.trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) :
(e₁.trans e₂) m = e₂ (e₁ m)
source
@[simp]
theorem AddEquiv.trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (m : M) :
(e₁.trans e₂) m = e₂ (e₁ m)
source
@[simp]
theorem MulEquiv.symm_trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Mul M] [Mul N] [Mul P] (e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) :
(e₁.trans e₂).symm p = e₁.symm (e₂.symm p)
source
@[simp]
theorem AddEquiv.symm_trans_apply {M : Type u_4} {N : Type u_5} {P : Type u_6} [Add M] [Add N] [Add P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) (p : P) :
(e₁.trans e₂).symm p = e₁.symm (e₂.symm p)
source
@[simp]
theorem MulEquiv.symm_trans_self {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
e.symm.trans e = refl N
source
@[simp]
theorem AddEquiv.symm_trans_self {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
e.symm.trans e = refl N
source
@[simp]
theorem MulEquiv.self_trans_symm {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (e : M ≃* N) :
e.trans e.symm = refl M
source
@[simp]
theorem AddEquiv.self_trans_symm {M : Type u_4} {N : Type u_5} [Add M] [Add N] (e : M ≃+ N) :
e.trans e.symm = refl M
source
def MulEquiv.symmEquiv (P : Type u_9) (Q : Type u_10) [Mul P] [Mul Q] :
P ≃* Q ≃ (Q ≃* P)

`MulEquiv.symm` defines an equivalence between `α ≃* β` and `β ≃* α`.

Equations

- MulEquiv.symmEquiv P Q = { toFun := MulEquiv.symm, invFun := MulEquiv.symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
def AddEquiv.symmEquiv (P : Type u_9) (Q : Type u_10) [Add P] [Add Q] :
P ≃+ Q ≃ (Q ≃+ P)

`AddEquiv.symm` defines an equivalence between `α ≃+ β` and `β ≃+ α`

Equations

- AddEquiv.symmEquiv P Q = { toFun := AddEquiv.symm, invFun := AddEquiv.symm, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem AddEquiv.symmEquiv_symm_apply_symm_apply (P : Type u_9) (Q : Type u_10) [Add P] [Add Q] (h : Q ≃+ P) (a✝ : Q) :
((symmEquiv P Q).symm h).symm a✝ = h a✝
source
@[simp]
theorem MulEquiv.symmEquiv_apply_symm_apply (P : Type u_9) (Q : Type u_10) [Mul P] [Mul Q] (h : P ≃* Q) (a✝ : P) :
((symmEquiv P Q) h).symm a✝ = h a✝
source
@[simp]
theorem MulEquiv.symmEquiv_symm_apply_symm_apply (P : Type u_9) (Q : Type u_10) [Mul P] [Mul Q] (h : Q ≃* P) (a✝ : Q) :
((symmEquiv P Q).symm h).symm a✝ = h a✝
source
@[simp]
theorem AddEquiv.symmEquiv_apply_apply (P : Type u_9) (Q : Type u_10) [Add P] [Add Q] (h : P ≃+ Q) (a✝ : Q) :
((symmEquiv P Q) h) a✝ = h.symm a✝
source
@[simp]
theorem AddEquiv.symmEquiv_symm_apply_apply (P : Type u_9) (Q : Type u_10) [Add P] [Add Q] (h : Q ≃+ P) (a✝ : P) :
((symmEquiv P Q).symm h) a✝ = h.symm a✝
source
@[simp]
theorem MulEquiv.symmEquiv_apply_apply (P : Type u_9) (Q : Type u_10) [Mul P] [Mul Q] (h : P ≃* Q) (a✝ : Q) :
((symmEquiv P Q) h) a✝ = h.symm a✝
source
@[simp]
theorem AddEquiv.symmEquiv_apply_symm_apply (P : Type u_9) (Q : Type u_10) [Add P] [Add Q] (h : P ≃+ Q) (a✝ : P) :
((symmEquiv P Q) h).symm a✝ = h a✝
source
@[simp]
theorem MulEquiv.symmEquiv_symm_apply_apply (P : Type u_9) (Q : Type u_10) [Mul P] [Mul Q] (h : Q ≃* P) (a✝ : P) :
((symmEquiv P Q).symm h) a✝ = h.symm a✝
source
def MulEquiv.cast {ι : Type u_9} {M : ι → Type u_10} [(i : ι) → Mul (M i)] {i j : ι} (h : i = j) :
M i ≃* M j

`Equiv.cast (congrArg _ h)` as a `MulEquiv`.

Note that unlike `Equiv.cast`, this takes an equality of indices rather than an equality of types, to avoid having to deal with an equality of the algebraic structure itself.

Equations

- MulEquiv.cast h = { toEquiv := Equiv.cast ⋯, map_mul' := ⋯ }

Instances For

source
def AddEquiv.cast {ι : Type u_9} {M : ι → Type u_10} [(i : ι) → Add (M i)] {i j : ι} (h : i = j) :
M i ≃+ M j

`Equiv.cast (congrArg _ h)` as an `AddEquiv`.

Note that unlike `Equiv.cast`, this takes an equality of indices rather than an equality of types, to avoid having to deal with an equality of the algebraic structure itself.

Equations

- AddEquiv.cast h = { toEquiv := Equiv.cast ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem MulEquiv.cast_symm_apply {ι : Type u_9} {M : ι → Type u_10} [(i : ι) → Mul (M i)] {i j : ι} (h : i = j) (a : M j) :
(MulEquiv.cast h).symm a = cast ⋯ a
source
@[simp]
theorem MulEquiv.cast_apply {ι : Type u_9} {M : ι → Type u_10} [(i : ι) → Mul (M i)] {i j : ι} (h : i = j) (a : M i) :
(MulEquiv.cast h) a = cast ⋯ a
source
@[simp]
theorem AddEquiv.cast_symm_apply {ι : Type u_9} {M : ι → Type u_10} [(i : ι) → Add (M i)] {i j : ι} (h : i = j) (a : M j) :
(AddEquiv.cast h).symm a = cast ⋯ a
source
@[simp]
theorem AddEquiv.cast_apply {ι : Type u_9} {M : ι → Type u_10} [(i : ι) → Add (M i)] {i j : ι} (h : i = j) (a : M i) :
(AddEquiv.cast h) a = cast ⋯ a

### Monoids #

source
@[simp]
theorem MulEquiv.coe_monoidHom_refl {M : Type u_4} [MulOneClass M] :
↑(refl M) = MonoidHom.id M
source
@[simp]
theorem AddEquiv.coe_addMonoidHom_refl {M : Type u_4} [AddZeroClass M] :
↑(refl M) = AddMonoidHom.id M
source
@[simp]
theorem MulEquiv.coe_monoidHom_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e₁ : M ≃* N) (e₂ : N ≃* P) :
↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
source
@[simp]
theorem AddEquiv.coe_addMonoidHom_trans {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e₁ : M ≃+ N) (e₂ : N ≃+ P) :
↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
source
@[simp]
theorem MulEquiv.coe_monoidHom_comp_coe_monoidHom_symm {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (e : M ≃* N) :
(↑e).comp ↑e.symm = MonoidHom.id N
source
@[simp]
theorem AddEquiv.coe_addMonoidHom_comp_coe_addMonoidHom_symm {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) :
(↑e).comp ↑e.symm = AddMonoidHom.id N
source
@[simp]
theorem MulEquiv.coe_monoidHom_symm_comp_coe_monoidHom {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (e : M ≃* N) :
(↑e.symm).comp ↑e = MonoidHom.id M
source
@[simp]
theorem AddEquiv.coe_addMonoidHom_symm_comp_coe_addMonoidHom {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) :
(↑e.symm).comp ↑e = AddMonoidHom.id M
source
theorem MulEquiv.comp_left_injective {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e : M ≃* N) :
Function.Injective fun (f : N →* P) => f.comp ↑e
source
theorem AddEquiv.comp_left_injective {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e : M ≃+ N) :
Function.Injective fun (f : N →+ P) => f.comp ↑e
source
theorem MulEquiv.comp_right_injective {M : Type u_4} {N : Type u_5} {P : Type u_6} [MulOneClass M] [MulOneClass N] [MulOneClass P] (e : M ≃* N) :
Function.Injective fun (f : P →* M) => (↑e).comp f
source
theorem AddEquiv.comp_right_injective {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (e : M ≃+ N) :
Function.Injective fun (f : P →+ M) => (↑e).comp f
source
theorem MulEquiv.map_one {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) :
h 1 = 1

A multiplicative isomorphism of monoids sends `1` to `1` (and is hence a monoid isomorphism).

source
theorem AddEquiv.map_zero {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) :
h 0 = 0

An additive isomorphism of additive monoids sends `0` to `0` (and is hence an additive monoid isomorphism).

source
theorem MulEquiv.map_eq_one_iff {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x : M} :
h x = 1 ↔ x = 1
source
theorem AddEquiv.map_eq_zero_iff {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) {x : M} :
h x = 0 ↔ x = 0
source
theorem MulEquiv.map_ne_one_iff {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) {x : M} :
h x ≠ 1 ↔ x ≠ 1
source
theorem AddEquiv.map_ne_zero_iff {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) {x : M} :
h x ≠ 0 ↔ x ≠ 0
source
noncomputable def MulEquiv.ofBijective {M : Type u_9} {N : Type u_10} {F : Type u_11} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) :
M ≃* N

A bijective `Semigroup` homomorphism is an isomorphism

Equations

- MulEquiv.ofBijective f hf = { toEquiv := Equiv.ofBijective (⇑f) hf, map_mul' := ⋯ }

Instances For

source
noncomputable def AddEquiv.ofBijective {M : Type u_9} {N : Type u_10} {F : Type u_11} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) :
M ≃+ N

A bijective `AddSemigroup` homomorphism is an isomorphism

Equations

- AddEquiv.ofBijective f hf = { toEquiv := Equiv.ofBijective (⇑f) hf, map_add' := ⋯ }

Instances For

source
@[simp]
theorem AddEquiv.ofBijective_apply {M : Type u_9} {N : Type u_10} {F : Type u_11} [Add M] [Add N] [FunLike F M N] [AddHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) (a : M) :
(ofBijective f hf) a = f a
source
@[simp]
theorem MulEquiv.ofBijective_apply {M : Type u_9} {N : Type u_10} {F : Type u_11} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] (f : F) (hf : Function.Bijective ⇑f) (a : M) :
(ofBijective f hf) a = f a
source
@[simp]
theorem MulEquiv.ofBijective_apply_symm_apply {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] {n : N} (f : M →* N) (hf : Function.Bijective ⇑f) :
f ((ofBijective f hf).symm n) = n
source
@[simp]
theorem AddEquiv.ofBijective_apply_symm_apply {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] {n : N} (f : M →+ N) (hf : Function.Bijective ⇑f) :
f ((ofBijective f hf).symm n) = n
source
def MulEquiv.toMonoidHom {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (h : M ≃* N) :
M →* N

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

Equations

- h.toMonoidHom = { toFun := h.toFun, map_one' := ⋯, map_mul' := ⋯ }

Instances For

source
def AddEquiv.toAddMonoidHom {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (h : M ≃+ N) :
M →+ N

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

Equations

- h.toAddMonoidHom = { toFun := h.toFun, map_zero' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem MulEquiv.coe_toMonoidHom {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (e : M ≃* N) :
⇑e.toMonoidHom = ⇑e
source
@[simp]
theorem AddEquiv.coe_toAddMonoidHom {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) :
⇑e.toAddMonoidHom = ⇑e
source
@[simp]
theorem MulEquiv.toMonoidHom_eq_coe {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M ≃* N) :
f.toMonoidHom = ↑f
source
@[simp]
theorem AddEquiv.toAddMonoidHom_eq_coe {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M ≃+ N) :
f.toAddMonoidHom = ↑f
source
theorem MulEquiv.toMonoidHom_injective {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] :
Function.Injective toMonoidHom
source
theorem AddEquiv.toAddMonoidHom_injective {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] :
Function.Injective toAddMonoidHom

### Groups #

source
theorem MulEquiv.map_inv {G : Type u_7} {H : Type u_8} [Group G] [DivisionMonoid H] (h : G ≃* H) (x : G) :
h x⁻¹ = (h x)⁻¹

A multiplicative equivalence of groups preserves inversion.

source
theorem AddEquiv.map_neg {G : Type u_7} {H : Type u_8} [AddGroup G] [SubtractionMonoid H] (h : G ≃+ H) (x : G) :
h (-x) = -h x

An additive equivalence of additive groups preserves negation.

source
theorem MulEquiv.map_div {G : Type u_7} {H : Type u_8} [Group G] [DivisionMonoid H] (h : G ≃* H) (x y : G) :
h (x / y) = h x / h y

A multiplicative equivalence of groups preserves division.

source
theorem AddEquiv.map_sub {G : Type u_7} {H : Type u_8} [AddGroup G] [SubtractionMonoid H] (h : G ≃+ H) (x y : G) :
h (x - y) = h x - h y

An additive equivalence of additive groups preserves subtractions.

source
def MulHom.toMulEquiv {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
M ≃* N

Given a pair of multiplicative homomorphisms `f`, `g` such that `g.comp f = id` and `f.comp g = id`, returns a multiplicative equivalence with `toFun = f` and `invFun = g`. This constructor is useful if the underlying type(s) have specialized `ext` lemmas for multiplicative homomorphisms.

Equations

- f.toMulEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source
def AddHom.toAddEquiv {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M →ₙ+ N) (g : N →ₙ+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
M ≃+ N

Given a pair of additive homomorphisms `f`, `g` such that `g.comp f = id` and `f.comp g = id`, returns an additive equivalence with `toFun = f` and `invFun = g`. This constructor is useful if the underlying type(s) have specialized `ext` lemmas for additive homomorphisms.

Equations

- f.toAddEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem MulHom.toMulEquiv_symm_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
⇑(f.toMulEquiv g h₁ h₂).symm = ⇑g
source
@[simp]
theorem AddHom.toAddEquiv_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M →ₙ+ N) (g : N →ₙ+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
⇑(f.toAddEquiv g h₁ h₂) = ⇑f
source
@[simp]
theorem AddHom.toAddEquiv_symm_apply {M : Type u_4} {N : Type u_5} [Add M] [Add N] (f : M →ₙ+ N) (g : N →ₙ+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
⇑(f.toAddEquiv g h₁ h₂).symm = ⇑g
source
@[simp]
theorem MulHom.toMulEquiv_apply {M : Type u_4} {N : Type u_5} [Mul M] [Mul N] (f : M →ₙ* N) (g : N →ₙ* M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
⇑(f.toMulEquiv g h₁ h₂) = ⇑f
source
def MonoidHom.toMulEquiv {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
M ≃* N

Given a pair of monoid homomorphisms `f`, `g` such that `g.comp f = id` and `f.comp g = id`, returns a multiplicative equivalence with `toFun = f` and `invFun = g`. This constructor is useful if the underlying type(s) have specialized `ext` lemmas for monoid homomorphisms.

Equations

- f.toMulEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

Instances For

source
def AddMonoidHom.toAddEquiv {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
M ≃+ N

Given a pair of additive monoid homomorphisms `f`, `g` such that `g.comp f = id` and `f.comp g = id`, returns an additive equivalence with `toFun = f` and `invFun = g`. This constructor is useful if the underlying type(s) have specialized `ext` lemmas for additive monoid homomorphisms.

Equations

- f.toAddEquiv g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem MonoidHom.toMulEquiv_symm_apply {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
⇑(f.toMulEquiv g h₁ h₂).symm = ⇑g
source
@[simp]
theorem AddMonoidHom.toAddEquiv_symm_apply {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
⇑(f.toAddEquiv g h₁ h₂).symm = ⇑g
source
@[simp]
theorem AddMonoidHom.toAddEquiv_apply {M : Type u_4} {N : Type u_5} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : N →+ M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
⇑(f.toAddEquiv g h₁ h₂) = ⇑f
source
@[simp]
theorem MonoidHom.toMulEquiv_apply {M : Type u_4} {N : Type u_5} [MulOneClass M] [MulOneClass N] (f : M →* N) (g : N →* M) (h₁ : g.comp f = id M) (h₂ : f.comp g = id N) :
⇑(f.toMulEquiv g h₁ h₂) = ⇑f