Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2018 Johannes HΓΆlzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes HΓΆlzl, Callum Sutton, Yury Kudryashov
Ported by: Scott Morrison

! This file was ported from Lean 3 source module algebra.hom.equiv.units.basic
! leanprover-community/mathlib commit a95b16cbade0f938fc24abd05412bde1e84bab9b
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Hom.Equiv.Basic
import Mathlib.Algebra.Hom.Units

/-!
# Multiplicative and additive equivalence acting on units.
-/

variable {
F: Type ?u.18158
F
Ξ±: Type ?u.38
Ξ±
Ξ²: Type ?u.41
Ξ²
A: Type ?u.15955
A
B: Type ?u.14
B
M: Type ?u.50
M
N: Type ?u.53
N
P: Type ?u.56
P
Q: Type ?u.11159
Q
G: Type ?u.17821
G
H: Type ?u.18188
H
:
Type _: Type (?u.16116+1)
Type _
} /-- A group is isomorphic to its group of units. -/ @[
to_additive: {G : Type u_1} β†’ [inst : AddGroup G] β†’ G ≃+ AddUnits G
to_additive
"An additive group is isomorphic to its group of additive units"] def
toUnits: [inst : Group G] β†’ G ≃* GΛ£
toUnits
[
Group: Type ?u.68 β†’ Type ?u.68
Group
G: Type ?u.62
G
] :
G: Type ?u.62
G
≃*
G: Type ?u.62
G
Λ£ where toFun
x: ?m.385
x
:= ⟨
x: ?m.385
x
,
x: ?m.385
x
⁻¹,
mul_inv_self: βˆ€ {G : Type ?u.467} [inst : Group G] (a : G), a * a⁻¹ = 1
mul_inv_self
_: ?m.468
_
,
inv_mul_self: βˆ€ {G : Type ?u.494} [inst : Group G] (a : G), a⁻¹ * a = 1
inv_mul_self
_: ?m.495
_
⟩ invFun
x: ?m.545
x
:=
x: ?m.545
x
left_inv
_: ?m.1265
_
:=
rfl: βˆ€ {Ξ± : Sort ?u.1267} {a : Ξ±}, a = a
rfl
right_inv
_: ?m.1278
_
:=
Units.ext: βˆ€ {Ξ± : Type ?u.1280} [inst : Monoid Ξ±], Function.Injective Units.val
Units.ext
rfl: βˆ€ {Ξ± : Sort ?u.1299} {a : Ξ±}, a = a
rfl
map_mul'
_: ?m.1305
_
_: ?m.1308
_
:=
Units.ext: βˆ€ {Ξ± : Type ?u.1310} [inst : Monoid Ξ±], Function.Injective Units.val
Units.ext
rfl: βˆ€ {Ξ± : Sort ?u.1328} {a : Ξ±}, a = a
rfl
#align to_units
toUnits: {G : Type u_1} β†’ [inst : Group G] β†’ G ≃* GΛ£
toUnits
#align to_add_units
toAddUnits: {G : Type u_1} β†’ [inst : AddGroup G] β†’ G ≃+ AddUnits G
toAddUnits
@[
to_additive: βˆ€ {G : Type u_1} [inst : AddGroup G] (g : G), ↑(↑toAddUnits g) = g
to_additive
(attr := simp)] theorem
coe_toUnits: βˆ€ {G : Type u_1} [inst : Group G] (g : G), ↑(↑toUnits g) = g
coe_toUnits
[
Group: Type ?u.1712 β†’ Type ?u.1712
Group
G: Type ?u.1706
G
] (
g: G
g
:
G: Type ?u.1706
G
) : (
toUnits: {G : Type ?u.1719} β†’ [inst : Group G] β†’ G ≃* GΛ£
toUnits
g: G
g
:
G: Type ?u.1706
G
) =
g: G
g
:=
rfl: βˆ€ {Ξ± : Sort ?u.2547} {a : Ξ±}, a = a
rfl
#align coe_to_units
coe_toUnits: βˆ€ {G : Type u_1} [inst : Group G] (g : G), ↑(↑toUnits g) = g
coe_toUnits
#align coe_to_add_units
coe_toAddUnits: βˆ€ {G : Type u_1} [inst : AddGroup G] (g : G), ↑(↑toAddUnits g) = g
coe_toAddUnits
namespace Units variable [
Monoid: Type ?u.5713 β†’ Type ?u.5713
Monoid
M: Type ?u.2634
M
] [
Monoid: Type ?u.11171 β†’ Type ?u.11171
Monoid
N: Type ?u.2637
N
] [
Monoid: Type ?u.2700 β†’ Type ?u.2700
Monoid
P: Type ?u.2640
P
] /-- A multiplicative equivalence of monoids defines a multiplicative equivalence of their groups of units. -/ def
mapEquiv: {M : Type u_1} β†’ {N : Type u_2} β†’ [inst : Monoid M] β†’ [inst_1 : Monoid N] β†’ M ≃* N β†’ MΛ£ ≃* NΛ£
mapEquiv
(
h: M ≃* N
h
:
M: Type ?u.2676
M
≃*
N: Type ?u.2679
N
) :
M: Type ?u.2676
M
Λ£ ≃*
N: Type ?u.2679
N
Λ£ := {
map: {M : Type ?u.2976} β†’ {N : Type ?u.2975} β†’ [inst : Monoid M] β†’ [inst_1 : Monoid N] β†’ (M β†’* N) β†’ MΛ£ β†’* NΛ£
map
h: M ≃* N
h
.
toMonoidHom: {M : Type ?u.3000} β†’ {N : Type ?u.2999} β†’ [inst : MulOneClass M] β†’ [inst_1 : MulOneClass N] β†’ M ≃* N β†’ M β†’* N
toMonoidHom
with invFun :=
map: {M : Type ?u.3307} β†’ {N : Type ?u.3306} β†’ [inst : Monoid M] β†’ [inst_1 : Monoid N] β†’ (M β†’* N) β†’ MΛ£ β†’* NΛ£
map
h: M ≃* N
h
.
symm: {M : Type ?u.3332} β†’ {N : Type ?u.3331} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ M ≃* N β†’ N ≃* M
symm
.
toMonoidHom: {M : Type ?u.3338} β†’ {N : Type ?u.3337} β†’ [inst : MulOneClass M] β†’ [inst_1 : MulOneClass N] β†’ M ≃* N β†’ M β†’* N
toMonoidHom
, left_inv := fun
u: ?m.3580
u
=>
ext: βˆ€ {Ξ± : Type ?u.3582} [inst : Monoid Ξ±], Function.Injective val
ext
<|
h: M ≃* N
h
.
left_inv: βˆ€ {Ξ± : Sort ?u.3608} {Ξ² : Sort ?u.3607} (self : Ξ± ≃ Ξ²), Function.LeftInverse self.invFun self.toFun
left_inv
u: ?m.3580
u
, right_inv := fun
u: ?m.4329
u
=>
ext: βˆ€ {Ξ± : Type ?u.4331} [inst : Monoid Ξ±], Function.Injective val
ext
<|
h: M ≃* N
h
.
right_inv: βˆ€ {Ξ± : Sort ?u.4357} {Ξ² : Sort ?u.4356} (self : Ξ± ≃ Ξ²), Function.RightInverse self.invFun self.toFun
right_inv
u: ?m.4329
u
} #align units.map_equiv
Units.mapEquiv: {M : Type u_1} β†’ {N : Type u_2} β†’ [inst : Monoid M] β†’ [inst_1 : Monoid N] β†’ M ≃* N β†’ MΛ£ ≃* NΛ£
Units.mapEquiv
@[simp] theorem
mapEquiv_symm: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (h : M ≃* N), MulEquiv.symm (mapEquiv h) = mapEquiv (MulEquiv.symm h)
mapEquiv_symm
(
h: M ≃* N
h
:
M: Type ?u.5259
M
≃*
N: Type ?u.5262
N
) : (
mapEquiv: {M : Type ?u.5440} β†’ {N : Type ?u.5439} β†’ [inst : Monoid M] β†’ [inst_1 : Monoid N] β†’ M ≃* N β†’ MΛ£ ≃* NΛ£
mapEquiv
h: M ≃* N
h
).
symm: {M : Type ?u.5478} β†’ {N : Type ?u.5477} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ M ≃* N β†’ N ≃* M
symm
=
mapEquiv: {M : Type ?u.5585} β†’ {N : Type ?u.5584} β†’ [inst : Monoid M] β†’ [inst_1 : Monoid N] β†’ M ≃* N β†’ MΛ£ ≃* NΛ£
mapEquiv
h: M ≃* N
h
.
symm: {M : Type ?u.5591} β†’ {N : Type ?u.5590} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ M ≃* N β†’ N ≃* M
symm
:=
rfl: βˆ€ {Ξ± : Sort ?u.5616} {a : Ξ±}, a = a
rfl
#align units.map_equiv_symm
Units.mapEquiv_symm: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (h : M ≃* N), MulEquiv.symm (mapEquiv h) = mapEquiv (MulEquiv.symm h)
Units.mapEquiv_symm
@[simp] theorem
coe_mapEquiv: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (h : M ≃* N) (x : MΛ£), ↑(↑(mapEquiv h) x) = ↑h ↑x
coe_mapEquiv
(
h: M ≃* N
h
:
M: Type ?u.5695
M
≃*
N: Type ?u.5698
N
) (
x: MΛ£
x
:
M: Type ?u.5695
M
Λ£) : (
mapEquiv: {M : Type ?u.5887} β†’ {N : Type ?u.5886} β†’ [inst : Monoid M] β†’ [inst_1 : Monoid N] β†’ M ≃* N β†’ MΛ£ ≃* NΛ£
mapEquiv
h: M ≃* N
h
x: MΛ£
x
:
N: Type ?u.5698
N
) =
h: M ≃* N
h
x: MΛ£
x
:=
rfl: βˆ€ {Ξ± : Sort ?u.7494} {a : Ξ±}, a = a
rfl
#align units.coe_map_equiv
Units.coe_mapEquiv: βˆ€ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (h : M ≃* N) (x : MΛ£), ↑(↑(mapEquiv h) x) = ↑h ↑x
Units.coe_mapEquiv
/-- Left multiplication by a unit of a monoid is a permutation of the underlying type. -/ @[
to_additive: {M : Type u_1} β†’ [inst : AddMonoid M] β†’ AddUnits M β†’ Equiv.Perm M
to_additive
(attr := simps (config := { fullyApplied :=
false: Bool
false
})
apply: βˆ€ {M : Type u_1} [inst : Monoid M] (u : MΛ£), ↑(mulLeft u) = fun x => ↑u * x
apply
) "Left addition of an additive unit is a permutation of the underlying type."] def
mulLeft: {M : Type u_1} β†’ [inst : Monoid M] β†’ MΛ£ β†’ Equiv.Perm M
mulLeft
(
u: MΛ£
u
:
M: Type ?u.7557
M
Λ£) :
Equiv.Perm: Sort ?u.7596 β†’ Sort (max1?u.7596)
Equiv.Perm
M: Type ?u.7557
M
where toFun
x: ?m.7607
x
:=
u: MΛ£
u
*
x: ?m.7607
x
invFun
x: ?m.9177
x
:=
u: MΛ£
u
⁻¹ *
x: ?m.9177
x
left_inv :=
u: MΛ£
u
.
inv_mul_cancel_left: βˆ€ {Ξ± : Type ?u.10656} [inst : Monoid Ξ±] (a : Ξ±Λ£) (b : Ξ±), ↑a⁻¹ * (↑a * b) = b
inv_mul_cancel_left
right_inv :=
u: MΛ£
u
.
mul_inv_cancel_left: βˆ€ {Ξ± : Type ?u.10675} [inst : Monoid Ξ±] (a : Ξ±Λ£) (b : Ξ±), ↑a * (↑a⁻¹ * b) = b
mul_inv_cancel_left
#align units.mul_left
Units.mulLeft: {M : Type u_1} β†’ [inst : Monoid M] β†’ MΛ£ β†’ Equiv.Perm M
Units.mulLeft
#align add_units.add_left
AddUnits.addLeft: {M : Type u_1} β†’ [inst : AddMonoid M] β†’ AddUnits M β†’ Equiv.Perm M
AddUnits.addLeft
#align units.mul_left_apply
Units.mulLeft_apply: βˆ€ {M : Type u_1} [inst : Monoid M] (u : MΛ£), ↑(mulLeft u) = fun x => ↑u * x
Units.mulLeft_apply
#align add_units.add_left_apply
AddUnits.addLeft_apply: βˆ€ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M), ↑(AddUnits.addLeft u) = fun x => ↑u + x
AddUnits.addLeft_apply
@[
to_additive: βˆ€ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M), (AddUnits.addLeft u).symm = AddUnits.addLeft (-u)
to_additive
(attr := simp)] theorem
mulLeft_symm: βˆ€ (u : MΛ£), (mulLeft u).symm = mulLeft u⁻¹
mulLeft_symm
(
u: MΛ£
u
:
M: Type ?u.11150
M
Λ£) :
u: MΛ£
u
.
mulLeft: {M : Type ?u.11190} β†’ [inst : Monoid M] β†’ MΛ£ β†’ Equiv.Perm M
mulLeft
.
symm: {Ξ± : Sort ?u.11196} β†’ {Ξ² : Sort ?u.11195} β†’ Ξ± ≃ Ξ² β†’ Ξ² ≃ Ξ±
symm
=
u: MΛ£
u
⁻¹.
mulLeft: {M : Type ?u.11221} β†’ [inst : Monoid M] β†’ MΛ£ β†’ Equiv.Perm M
mulLeft
:=
Equiv.ext: βˆ€ {Ξ± : Sort ?u.11231} {Ξ² : Sort ?u.11230} {f g : Ξ± ≃ Ξ²}, (βˆ€ (x : Ξ±), ↑f x = ↑g x) β†’ f = g
Equiv.ext
fun
_: ?m.11242
_
=>
rfl: βˆ€ {Ξ± : Sort ?u.11244} {a : Ξ±}, a = a
rfl
#align units.mul_left_symm
Units.mulLeft_symm: βˆ€ {M : Type u_1} [inst : Monoid M] (u : MΛ£), (mulLeft u).symm = mulLeft u⁻¹
Units.mulLeft_symm
#align add_units.add_left_symm
AddUnits.addLeft_symm: βˆ€ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M), (AddUnits.addLeft u).symm = AddUnits.addLeft (-u)
AddUnits.addLeft_symm
@[
to_additive: βˆ€ {M : Type u_1} [inst : AddMonoid M] (a : AddUnits M), Function.Bijective fun x => ↑a + x
to_additive
] theorem
mulLeft_bijective: βˆ€ (a : MΛ£), Function.Bijective fun x => ↑a * x
mulLeft_bijective
(
a: MΛ£
a
:
M: Type ?u.11311
M
Λ£) :
Function.Bijective: {Ξ± : Sort ?u.11351} β†’ {Ξ² : Sort ?u.11350} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Bijective
((
a: MΛ£
a
* Β·) :
M: Type ?u.11311
M
β†’
M: Type ?u.11311
M
) := (
mulLeft: {M : Type ?u.12935} β†’ [inst : Monoid M] β†’ MΛ£ β†’ Equiv.Perm M
mulLeft
a: MΛ£
a
).
bijective: βˆ€ {Ξ± : Sort ?u.12951} {Ξ² : Sort ?u.12950} (e : Ξ± ≃ Ξ²), Function.Bijective ↑e
bijective
#align units.mul_left_bijective
Units.mulLeft_bijective: βˆ€ {M : Type u_1} [inst : Monoid M] (a : MΛ£), Function.Bijective fun x => ↑a * x
Units.mulLeft_bijective
#align add_units.add_left_bijective
AddUnits.addLeft_bijective: βˆ€ {M : Type u_1} [inst : AddMonoid M] (a : AddUnits M), Function.Bijective fun x => ↑a + x
AddUnits.addLeft_bijective
/-- Right multiplication by a unit of a monoid is a permutation of the underlying type. -/ @[
to_additive: {M : Type u_1} β†’ [inst : AddMonoid M] β†’ AddUnits M β†’ Equiv.Perm M
to_additive
(attr := simps (config := { fullyApplied :=
false: Bool
false
})
apply: βˆ€ {M : Type u_1} [inst : Monoid M] (u : MΛ£), ↑(mulRight u) = fun x => x * ↑u
apply
) "Right addition of an additive unit is a permutation of the underlying type."] def
mulRight: {M : Type u_1} β†’ [inst : Monoid M] β†’ MΛ£ β†’ Equiv.Perm M
mulRight
(
u: MΛ£
u
:
M: Type ?u.12998
M
Λ£) :
Equiv.Perm: Sort ?u.13037 β†’ Sort (max1?u.13037)
Equiv.Perm
M: Type ?u.12998
M
where toFun
x: ?m.13048
x
:=
x: ?m.13048
x
*
u: MΛ£
u
invFun
x: ?m.14618
x
:=
x: ?m.14618
x
* ↑
u: MΛ£
u
⁻¹ left_inv
x: ?m.14699
x
:=
mul_inv_cancel_right: βˆ€ {Ξ± : Type ?u.14701} [inst : Monoid Ξ±] (a : Ξ±) (b : Ξ±Λ£), a * ↑b * ↑b⁻¹ = a
mul_inv_cancel_right
x: ?m.14699
x
u: MΛ£
u
right_inv
x: ?m.14753
x
:=
inv_mul_cancel_right: βˆ€ {Ξ± : Type ?u.14755} [inst : Monoid Ξ±] (a : Ξ±) (b : Ξ±Λ£), a * ↑b⁻¹ * ↑b = a
inv_mul_cancel_right
x: ?m.14753
x
u: MΛ£
u
#align units.mul_right
Units.mulRight: {M : Type u_1} β†’ [inst : Monoid M] β†’ MΛ£ β†’ Equiv.Perm M
Units.mulRight
#align add_units.add_right
AddUnits.addRight: {M : Type u_1} β†’ [inst : AddMonoid M] β†’ AddUnits M β†’ Equiv.Perm M
AddUnits.addRight
#align units.mul_right_apply
Units.mulRight_apply: βˆ€ {M : Type u_1} [inst : Monoid M] (u : MΛ£), ↑(mulRight u) = fun x => x * ↑u
Units.mulRight_apply
#align add_units.add_right_apply
AddUnits.addRight_apply: βˆ€ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M), ↑(AddUnits.addRight u) = fun x => x + ↑u
AddUnits.addRight_apply
@[
to_additive: βˆ€ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M), (AddUnits.addRight u).symm = AddUnits.addRight (-u)
to_additive
(attr := simp)] theorem
mulRight_symm: βˆ€ {M : Type u_1} [inst : Monoid M] (u : MΛ£), (mulRight u).symm = mulRight u⁻¹
mulRight_symm
(
u: MΛ£
u
:
M: Type ?u.15961
M
Λ£) :
u: MΛ£
u
.
mulRight: {M : Type ?u.16001} β†’ [inst : Monoid M] β†’ MΛ£ β†’ Equiv.Perm M
mulRight
.
symm: {Ξ± : Sort ?u.16007} β†’ {Ξ² : Sort ?u.16006} β†’ Ξ± ≃ Ξ² β†’ Ξ² ≃ Ξ±
symm
=
u: MΛ£
u
⁻¹.
mulRight: {M : Type ?u.16032} β†’ [inst : Monoid M] β†’ MΛ£ β†’ Equiv.Perm M
mulRight
:=
Equiv.ext: βˆ€ {Ξ± : Sort ?u.16042} {Ξ² : Sort ?u.16041} {f g : Ξ± ≃ Ξ²}, (βˆ€ (x : Ξ±), ↑f x = ↑g x) β†’ f = g
Equiv.ext
fun
_: ?m.16053
_
=>
rfl: βˆ€ {Ξ± : Sort ?u.16055} {a : Ξ±}, a = a
rfl
#align units.mul_right_symm
Units.mulRight_symm: βˆ€ {M : Type u_1} [inst : Monoid M] (u : MΛ£), (mulRight u).symm = mulRight u⁻¹
Units.mulRight_symm
#align add_units.add_right_symm
AddUnits.addRight_symm: βˆ€ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M), (AddUnits.addRight u).symm = AddUnits.addRight (-u)
AddUnits.addRight_symm
@[
to_additive: βˆ€ {M : Type u_1} [inst : AddMonoid M] (a : AddUnits M), Function.Bijective fun x => x + ↑a
to_additive
] theorem
mulRight_bijective: βˆ€ {M : Type u_1} [inst : Monoid M] (a : MΛ£), Function.Bijective fun x => x * ↑a
mulRight_bijective
(
a: MΛ£
a
:
M: Type ?u.16122
M
Λ£) :
Function.Bijective: {Ξ± : Sort ?u.16162} β†’ {Ξ² : Sort ?u.16161} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Bijective
((Β· *
a: MΛ£
a
) :
M: Type ?u.16122
M
β†’
M: Type ?u.16122
M
) := (
mulRight: {M : Type ?u.17746} β†’ [inst : Monoid M] β†’ MΛ£ β†’ Equiv.Perm M
mulRight
a: MΛ£
a
).
bijective: βˆ€ {Ξ± : Sort ?u.17762} {Ξ² : Sort ?u.17761} (e : Ξ± ≃ Ξ²), Function.Bijective ↑e
bijective
#align units.mul_right_bijective
Units.mulRight_bijective: βˆ€ {M : Type u_1} [inst : Monoid M] (a : MΛ£), Function.Bijective fun x => x * ↑a
Units.mulRight_bijective
#align add_units.add_right_bijective
AddUnits.addRight_bijective: βˆ€ {M : Type u_1} [inst : AddMonoid M] (a : AddUnits M), Function.Bijective fun x => x + ↑a
AddUnits.addRight_bijective
end Units namespace Equiv section Group variable [
Group: Type ?u.19028 β†’ Type ?u.19028
Group
G: Type ?u.18185
G
] /-- Left multiplication in a `Group` is a permutation of the underlying type. -/ @[
to_additive: {G : Type u_1} β†’ [inst : AddGroup G] β†’ G β†’ Perm G
to_additive
"Left addition in an `AddGroup` is a permutation of the underlying type."] protected def
mulLeft: G β†’ Perm G
mulLeft
(
a: G
a
:
G: Type ?u.17857
G
) :
Perm: Sort ?u.17868 β†’ Sort (max1?u.17868)
Perm
G: Type ?u.17857
G
:= (
toUnits: {G : Type ?u.17872} β†’ [inst : Group G] β†’ G ≃* GΛ£
toUnits
a: G
a
).
mulLeft: {M : Type ?u.17921} β†’ [inst : Monoid M] β†’ MΛ£ β†’ Perm M
mulLeft
#align equiv.mul_left
Equiv.mulLeft: {G : Type u_1} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulLeft
#align equiv.add_left
Equiv.addLeft: {G : Type u_1} β†’ [inst : AddGroup G] β†’ G β†’ Perm G
Equiv.addLeft
@[
to_additive: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), ↑(Equiv.addLeft a) = (fun x x_1 => x + x_1) a
to_additive
(attr := simp)] theorem
coe_mulLeft: βˆ€ (a : G), ↑(Equiv.mulLeft a) = (fun x x_1 => x * x_1) a
coe_mulLeft
(
a: G
a
:
G: Type ?u.18185
G
) : ⇑(
Equiv.mulLeft: {G : Type ?u.18197} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulLeft
a: G
a
) =
(Β· * Β·): G β†’ G β†’ G
(Β· * Β·)
a: G
a
:=
rfl: βˆ€ {Ξ± : Sort ?u.18483} {a : Ξ±}, a = a
rfl
#align equiv.coe_mul_left
Equiv.coe_mulLeft: βˆ€ {G : Type u_1} [inst : Group G] (a : G), ↑(Equiv.mulLeft a) = (fun x x_1 => x * x_1) a
Equiv.coe_mulLeft
#align equiv.coe_add_left
Equiv.coe_addLeft: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), ↑(Equiv.addLeft a) = (fun x x_1 => x + x_1) a
Equiv.coe_addLeft
-- Porting note: we don't put `@[simp]` on the additive version; -- mysteriously simp can already prove that one (although not the multiplicative one)! /-- Extra simp lemma that `dsimp` can use. `simp` will never use this. -/ @[
to_additive: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), ↑(Equiv.addLeft a).symm = fun x => -a + x
to_additive
"Extra simp lemma that `dsimp` can use. `simp` will never use this.", simp, nolint simpNF] theorem
mulLeft_symm_apply: βˆ€ (a : G), ↑(Equiv.mulLeft a).symm = fun x => a⁻¹ * x
mulLeft_symm_apply
(
a: G
a
:
G: Type ?u.18588
G
) : ((
Equiv.mulLeft: {G : Type ?u.18603} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulLeft
a: G
a
).
symm: {Ξ± : Sort ?u.18611} β†’ {Ξ² : Sort ?u.18610} β†’ Ξ± ≃ Ξ² β†’ Ξ² ≃ Ξ±
symm
:
G: Type ?u.18588
G
β†’
G: Type ?u.18588
G
) = (
a: G
a
⁻¹ * ·) :=
rfl: βˆ€ {Ξ± : Sort ?u.18935} {a : Ξ±}, a = a
rfl
#align equiv.mul_left_symm_apply
Equiv.mulLeft_symm_apply: βˆ€ {G : Type u_1} [inst : Group G] (a : G), ↑(Equiv.mulLeft a).symm = fun x => a⁻¹ * x
Equiv.mulLeft_symm_apply
#align equiv.add_left_symm_apply
Equiv.addLeft_symm_apply: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), ↑(Equiv.addLeft a).symm = fun x => -a + x
Equiv.addLeft_symm_apply
@[
to_additive: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), (Equiv.addLeft a).symm = Equiv.addLeft (-a)
to_additive
(attr := simp)] theorem
mulLeft_symm: βˆ€ (a : G), (Equiv.mulLeft a).symm = Equiv.mulLeft a⁻¹
mulLeft_symm
(
a: G
a
:
G: Type ?u.19022
G
) : (
Equiv.mulLeft: {G : Type ?u.19034} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulLeft
a: G
a
).
symm: {Ξ± : Sort ?u.19042} β†’ {Ξ² : Sort ?u.19041} β†’ Ξ± ≃ Ξ² β†’ Ξ² ≃ Ξ±
symm
=
Equiv.mulLeft: {G : Type ?u.19050} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulLeft
a: G
a
⁻¹ :=
ext: βˆ€ {Ξ± : Sort ?u.19118} {Ξ² : Sort ?u.19117} {f g : Ξ± ≃ Ξ²}, (βˆ€ (x : Ξ±), ↑f x = ↑g x) β†’ f = g
ext
fun
_: ?m.19129
_
=>
rfl: βˆ€ {Ξ± : Sort ?u.19131} {a : Ξ±}, a = a
rfl
#align equiv.mul_left_symm
Equiv.mulLeft_symm: βˆ€ {G : Type u_1} [inst : Group G] (a : G), (Equiv.mulLeft a).symm = Equiv.mulLeft a⁻¹
Equiv.mulLeft_symm
#align equiv.add_left_symm
Equiv.addLeft_symm: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), (Equiv.addLeft a).symm = Equiv.addLeft (-a)
Equiv.addLeft_symm
@[
to_additive: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), Function.Bijective fun x => a + x
to_additive
] theorem
_root_.Group.mulLeft_bijective: βˆ€ (a : G), Function.Bijective fun x => a * x
_root_.Group.mulLeft_bijective
(
a: G
a
:
G: Type ?u.19212
G
) :
Function.Bijective: {Ξ± : Sort ?u.19224} β†’ {Ξ² : Sort ?u.19223} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Bijective
(
a: G
a
* Β·) := (
Equiv.mulLeft: {G : Type ?u.19420} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulLeft
a: G
a
).
bijective: βˆ€ {Ξ± : Sort ?u.19428} {Ξ² : Sort ?u.19427} (e : Ξ± ≃ Ξ²), Function.Bijective ↑e
bijective
#align group.mul_left_bijective
Group.mulLeft_bijective: βˆ€ {G : Type u_1} [inst : Group G] (a : G), Function.Bijective fun x => a * x
Group.mulLeft_bijective
#align add_group.add_left_bijective
AddGroup.addLeft_bijective: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), Function.Bijective fun x => a + x
AddGroup.addLeft_bijective
/-- Right multiplication in a `Group` is a permutation of the underlying type. -/ @[
to_additive: {G : Type u_1} β†’ [inst : AddGroup G] β†’ G β†’ Perm G
to_additive
"Right addition in an `AddGroup` is a permutation of the underlying type."] protected def
mulRight: {G : Type u_1} β†’ [inst : Group G] β†’ G β†’ Perm G
mulRight
(
a: G
a
:
G: Type ?u.19489
G
) :
Perm: Sort ?u.19500 β†’ Sort (max1?u.19500)
Perm
G: Type ?u.19489
G
:= (
toUnits: {G : Type ?u.19504} β†’ [inst : Group G] β†’ G ≃* GΛ£
toUnits
a: G
a
).
mulRight: {M : Type ?u.19553} β†’ [inst : Monoid M] β†’ MΛ£ β†’ Perm M
mulRight
#align equiv.mul_right
Equiv.mulRight: {G : Type u_1} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulRight
#align equiv.add_right
Equiv.addRight: {G : Type u_1} β†’ [inst : AddGroup G] β†’ G β†’ Perm G
Equiv.addRight
@[
to_additive: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), ↑(Equiv.addRight a) = fun x => x + a
to_additive
(attr := simp)] theorem
coe_mulRight: βˆ€ (a : G), ↑(Equiv.mulRight a) = fun x => x * a
coe_mulRight
(
a: G
a
:
G: Type ?u.19775
G
) : ⇑(
Equiv.mulRight: {G : Type ?u.19787} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulRight
a: G
a
) = fun
x: ?m.19874
x
=>
x: ?m.19874
x
*
a: G
a
:=
rfl: βˆ€ {Ξ± : Sort ?u.20070} {a : Ξ±}, a = a
rfl
#align equiv.coe_mul_right
Equiv.coe_mulRight: βˆ€ {G : Type u_1} [inst : Group G] (a : G), ↑(Equiv.mulRight a) = fun x => x * a
Equiv.coe_mulRight
#align equiv.coe_add_right
Equiv.coe_addRight: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), ↑(Equiv.addRight a) = fun x => x + a
Equiv.coe_addRight
@[
to_additive: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), (Equiv.addRight a).symm = Equiv.addRight (-a)
to_additive
(attr := simp)] theorem
mulRight_symm: βˆ€ (a : G), (Equiv.mulRight a).symm = Equiv.mulRight a⁻¹
mulRight_symm
(
a: G
a
:
G: Type ?u.20172
G
) : (
Equiv.mulRight: {G : Type ?u.20184} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulRight
a: G
a
).
symm: {Ξ± : Sort ?u.20192} β†’ {Ξ² : Sort ?u.20191} β†’ Ξ± ≃ Ξ² β†’ Ξ² ≃ Ξ±
symm
=
Equiv.mulRight: {G : Type ?u.20200} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulRight
a: G
a
⁻¹ :=
ext: βˆ€ {Ξ± : Sort ?u.20268} {Ξ² : Sort ?u.20267} {f g : Ξ± ≃ Ξ²}, (βˆ€ (x : Ξ±), ↑f x = ↑g x) β†’ f = g
ext
fun
_: ?m.20279
_
=>
rfl: βˆ€ {Ξ± : Sort ?u.20281} {a : Ξ±}, a = a
rfl
#align equiv.mul_right_symm
Equiv.mulRight_symm: βˆ€ {G : Type u_1} [inst : Group G] (a : G), (Equiv.mulRight a).symm = Equiv.mulRight a⁻¹
Equiv.mulRight_symm
#align equiv.add_right_symm
Equiv.addRight_symm: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), (Equiv.addRight a).symm = Equiv.addRight (-a)
Equiv.addRight_symm
/-- Extra simp lemma that `dsimp` can use. `simp` will never use this. -/ @[
to_additive: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), ↑(Equiv.addRight a).symm = fun x => x + -a
to_additive
"Extra simp lemma that `dsimp` can use. `simp` will never use this.", simp, nolint simpNF] theorem
mulRight_symm_apply: βˆ€ {G : Type u_1} [inst : Group G] (a : G), ↑(Equiv.mulRight a).symm = fun x => x * a⁻¹
mulRight_symm_apply
(
a: G
a
:
G: Type ?u.20362
G
) : ((
Equiv.mulRight: {G : Type ?u.20377} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulRight
a: G
a
).
symm: {Ξ± : Sort ?u.20385} β†’ {Ξ² : Sort ?u.20384} β†’ Ξ± ≃ Ξ² β†’ Ξ² ≃ Ξ±
symm
:
G: Type ?u.20362
G
β†’
G: Type ?u.20362
G
) = fun
x: ?m.20469
x
=>
x: ?m.20469
x
*
a: G
a
⁻¹ :=
rfl: βˆ€ {Ξ± : Sort ?u.20709} {a : Ξ±}, a = a
rfl
#align equiv.mul_right_symm_apply
Equiv.mulRight_symm_apply: βˆ€ {G : Type u_1} [inst : Group G] (a : G), ↑(Equiv.mulRight a).symm = fun x => x * a⁻¹
Equiv.mulRight_symm_apply
#align equiv.add_right_symm_apply
Equiv.addRight_symm_apply: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), ↑(Equiv.addRight a).symm = fun x => x + -a
Equiv.addRight_symm_apply
@[
to_additive: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), Function.Bijective fun x => x + a
to_additive
] theorem
_root_.Group.mulRight_bijective: βˆ€ (a : G), Function.Bijective fun x => x * a
_root_.Group.mulRight_bijective
(
a: G
a
:
G: Type ?u.20796
G
) :
Function.Bijective: {Ξ± : Sort ?u.20808} β†’ {Ξ² : Sort ?u.20807} β†’ (Ξ± β†’ Ξ²) β†’ Prop
Function.Bijective
(Β· *
a: G
a
) := (
Equiv.mulRight: {G : Type ?u.21004} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulRight
a: G
a
).
bijective: βˆ€ {Ξ± : Sort ?u.21012} {Ξ² : Sort ?u.21011} (e : Ξ± ≃ Ξ²), Function.Bijective ↑e
bijective
#align group.mul_right_bijective
Group.mulRight_bijective: βˆ€ {G : Type u_1} [inst : Group G] (a : G), Function.Bijective fun x => x * a
Group.mulRight_bijective
#align add_group.add_right_bijective
AddGroup.addRight_bijective: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), Function.Bijective fun x => x + a
AddGroup.addRight_bijective
/-- A version of `Equiv.mulLeft a b⁻¹` that is defeq to `a / b`. -/ @[
to_additive: {G : Type u_1} β†’ [inst : AddGroup G] β†’ G β†’ G ≃ G
to_additive
(attr :=
simps: βˆ€ {G : Type u_1} [inst : AddGroup G] (a b : G), ↑(Equiv.subLeft a).symm b = -b + a
simps
) " A version of `Equiv.addLeft a (-b)` that is defeq to `a - b`. "] protected def
divLeft: G β†’ G ≃ G
divLeft
(
a: G
a
:
G: Type ?u.21073
G
) :
G: Type ?u.21073
G
≃
G: Type ?u.21073
G
where toFun
b: ?m.21095
b
:=
a: G
a
/
b: ?m.21095
b
invFun
b: ?m.21183
b
:=
b: ?m.21183
b
⁻¹ *
a: G
a
left_inv
b: ?m.21410
b
:=

Goals accomplished! πŸ™
F: Type ?u.21046

Ξ±: Type ?u.21049

Ξ²: Type ?u.21052

A: Type ?u.21055

B: Type ?u.21058

M: Type ?u.21061

N: Type ?u.21064

P: Type ?u.21067

Q: Type ?u.21070

G: Type ?u.21073

H: Type ?u.21076

inst✝: Group G

a, b: G


(fun b => b⁻¹ * a) ((fun b => a / b) b) = b

Goals accomplished! πŸ™
right_inv
b: ?m.21416
b
:=

Goals accomplished! πŸ™
F: Type ?u.21046

Ξ±: Type ?u.21049

Ξ²: Type ?u.21052

A: Type ?u.21055

B: Type ?u.21058

M: Type ?u.21061

N: Type ?u.21064

P: Type ?u.21067

Q: Type ?u.21070

G: Type ?u.21073

H: Type ?u.21076

inst✝: Group G

a, b: G


(fun b => a / b) ((fun b => b⁻¹ * a) b) = b

Goals accomplished! πŸ™
#align equiv.div_left
Equiv.divLeft: {G : Type u_1} β†’ [inst : Group G] β†’ G β†’ G ≃ G
Equiv.divLeft
#align equiv.sub_left
Equiv.subLeft: {G : Type u_1} β†’ [inst : AddGroup G] β†’ G β†’ G ≃ G
Equiv.subLeft
#align equiv.div_left_apply
Equiv.divLeft_apply: βˆ€ {G : Type u_1} [inst : Group G] (a b : G), ↑(Equiv.divLeft a) b = a / b
Equiv.divLeft_apply
#align equiv.div_left_symm_apply
Equiv.divLeft_symm_apply: βˆ€ {G : Type u_1} [inst : Group G] (a b : G), ↑(Equiv.divLeft a).symm b = b⁻¹ * a
Equiv.divLeft_symm_apply
#align equiv.sub_left_apply
Equiv.subLeft_apply: βˆ€ {G : Type u_1} [inst : AddGroup G] (a b : G), ↑(Equiv.subLeft a) b = a - b
Equiv.subLeft_apply
#align equiv.sub_left_symm_apply
Equiv.subLeft_symm_apply: βˆ€ {G : Type u_1} [inst : AddGroup G] (a b : G), ↑(Equiv.subLeft a).symm b = -b + a
Equiv.subLeft_symm_apply
@[
to_additive: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), Equiv.subLeft a = (Equiv.neg G).trans (Equiv.addLeft a)
to_additive
] theorem
divLeft_eq_inv_trans_mulLeft: βˆ€ (a : G), Equiv.divLeft a = (Equiv.inv G).trans (Equiv.mulLeft a)
divLeft_eq_inv_trans_mulLeft
(
a: G
a
:
G: Type ?u.22727
G
) :
Equiv.divLeft: {G : Type ?u.22739} β†’ [inst : Group G] β†’ G β†’ G ≃ G
Equiv.divLeft
a: G
a
= (
Equiv.inv: (G : Type ?u.22746) β†’ [inst : InvolutiveInv G] β†’ Perm G
Equiv.inv
G: Type ?u.22727
G
).
trans: {Ξ± : Sort ?u.22771} β†’ {Ξ² : Sort ?u.22770} β†’ {Ξ³ : Sort ?u.22769} β†’ Ξ± ≃ Ξ² β†’ Ξ² ≃ Ξ³ β†’ Ξ± ≃ Ξ³
trans
(
Equiv.mulLeft: {G : Type ?u.22782} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulLeft
a: G
a
) :=
ext: βˆ€ {Ξ± : Sort ?u.22795} {Ξ² : Sort ?u.22794} {f g : Ξ± ≃ Ξ²}, (βˆ€ (x : Ξ±), ↑f x = ↑g x) β†’ f = g
ext
fun
_: ?m.22806
_
=>
div_eq_mul_inv: βˆ€ {G : Type ?u.22808} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
div_eq_mul_inv
_: ?m.22809
_
_: ?m.22809
_
#align equiv.div_left_eq_inv_trans_mul_left
Equiv.divLeft_eq_inv_trans_mulLeft: βˆ€ {G : Type u_1} [inst : Group G] (a : G), Equiv.divLeft a = (Equiv.inv G).trans (Equiv.mulLeft a)
Equiv.divLeft_eq_inv_trans_mulLeft
#align equiv.sub_left_eq_neg_trans_add_left
Equiv.subLeft_eq_neg_trans_addLeft: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), Equiv.subLeft a = (Equiv.neg G).trans (Equiv.addLeft a)
Equiv.subLeft_eq_neg_trans_addLeft
/-- A version of `Equiv.mulRight a⁻¹ b` that is defeq to `b / a`. -/ @[
to_additive: {G : Type u_1} β†’ [inst : AddGroup G] β†’ G β†’ G ≃ G
to_additive
(attr :=
simps: βˆ€ {G : Type u_1} [inst : Group G] (a b : G), ↑(Equiv.divRight a).symm b = b * a
simps
) " A version of `Equiv.addRight (-a) b` that is defeq to `b - a`. "] protected def
divRight: G β†’ G ≃ G
divRight
(
a: G
a
:
G: Type ?u.22924
G
) :
G: Type ?u.22924
G
≃
G: Type ?u.22924
G
where toFun
b: ?m.22946
b
:=
b: ?m.22946
b
/
a: G
a
invFun
b: ?m.23034
b
:=
b: ?m.23034
b
*
a: G
a
left_inv
b: ?m.23217
b
:=

Goals accomplished! πŸ™
F: Type ?u.22897

Ξ±: Type ?u.22900

Ξ²: Type ?u.22903

A: Type ?u.22906

B: Type ?u.22909

M: Type ?u.22912

N: Type ?u.22915

P: Type ?u.22918

Q: Type ?u.22921

G: Type ?u.22924

H: Type ?u.22927

inst✝: Group G

a, b: G


(fun b => b * a) ((fun b => b / a) b) = b

Goals accomplished! πŸ™
right_inv
b: ?m.23223
b
:=

Goals accomplished! πŸ™
F: Type ?u.22897

Ξ±: Type ?u.22900

Ξ²: Type ?u.22903

A: Type ?u.22906

B: Type ?u.22909

M: Type ?u.22912

N: Type ?u.22915

P: Type ?u.22918

Q: Type ?u.22921

G: Type ?u.22924

H: Type ?u.22927

inst✝: Group G

a, b: G


(fun b => b / a) ((fun b => b * a) b) = b

Goals accomplished! πŸ™
#align equiv.div_right
Equiv.divRight: {G : Type u_1} β†’ [inst : Group G] β†’ G β†’ G ≃ G
Equiv.divRight
#align equiv.sub_right
Equiv.subRight: {G : Type u_1} β†’ [inst : AddGroup G] β†’ G β†’ G ≃ G
Equiv.subRight
#align equiv.div_right_symm_apply
Equiv.divRight_symm_apply: βˆ€ {G : Type u_1} [inst : Group G] (a b : G), ↑(Equiv.divRight a).symm b = b * a
Equiv.divRight_symm_apply
#align equiv.div_right_apply
Equiv.divRight_apply: βˆ€ {G : Type u_1} [inst : Group G] (a b : G), ↑(Equiv.divRight a) b = b / a
Equiv.divRight_apply
#align equiv.sub_right_symm_apply
Equiv.subRight_symm_apply: βˆ€ {G : Type u_1} [inst : AddGroup G] (a b : G), ↑(Equiv.subRight a).symm b = b + a
Equiv.subRight_symm_apply
#align equiv.sub_right_apply
Equiv.subRight_apply: βˆ€ {G : Type u_1} [inst : AddGroup G] (a b : G), ↑(Equiv.subRight a) b = b - a
Equiv.subRight_apply
@[
to_additive: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), Equiv.subRight a = Equiv.addRight (-a)
to_additive
] theorem
divRight_eq_mulRight_inv: βˆ€ {G : Type u_1} [inst : Group G] (a : G), Equiv.divRight a = Equiv.mulRight a⁻¹
divRight_eq_mulRight_inv
(
a: G
a
:
G: Type ?u.23969
G
) :
Equiv.divRight: {G : Type ?u.23981} β†’ [inst : Group G] β†’ G β†’ G ≃ G
Equiv.divRight
a: G
a
=
Equiv.mulRight: {G : Type ?u.23988} β†’ [inst : Group G] β†’ G β†’ Perm G
Equiv.mulRight
a: G
a
⁻¹ :=
ext: βˆ€ {Ξ± : Sort ?u.24056} {Ξ² : Sort ?u.24055} {f g : Ξ± ≃ Ξ²}, (βˆ€ (x : Ξ±), ↑f x = ↑g x) β†’ f = g
ext
fun
_: ?m.24067
_
=>
div_eq_mul_inv: βˆ€ {G : Type ?u.24069} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹
div_eq_mul_inv
_: ?m.24070
_
_: ?m.24070
_
#align equiv.div_right_eq_mul_right_inv
Equiv.divRight_eq_mulRight_inv: βˆ€ {G : Type u_1} [inst : Group G] (a : G), Equiv.divRight a = Equiv.mulRight a⁻¹
Equiv.divRight_eq_mulRight_inv
#align equiv.sub_right_eq_add_right_neg
Equiv.subRight_eq_addRight_neg: βˆ€ {G : Type u_1} [inst : AddGroup G] (a : G), Equiv.subRight a = Equiv.addRight (-a)
Equiv.subRight_eq_addRight_neg
end Group end Equiv -- Porting note: we don't put `@[simp]` on the additive version; -- mysteriously simp can already prove that one (although not the multiplicative one)! -- porting note: `@[simps apply]` removed because right now it's generating lemmas which -- aren't in simp normal form (they contain a `toFun`) /-- In a `DivisionCommMonoid`, `Equiv.inv` is a `MulEquiv`. There is a variant of this `MulEquiv.inv' G : G ≃* Gᡐᡒᡖ` for the non-commutative case. -/ @[
to_additive: (G : Type u_1) β†’ [inst : SubtractionCommMonoid G] β†’ G ≃+ G
to_additive
(attr := simps
apply: βˆ€ (G : Type u_1) [inst : DivisionCommMonoid G] (a : G), ↑(inv G) a = a⁻¹
apply
) "When the `AddGroup` is commutative, `Equiv.neg` is an `AddEquiv`."] def
MulEquiv.inv: (G : Type ?u.24191) β†’ [inst : DivisionCommMonoid G] β†’ G ≃* G
MulEquiv.inv
(
G: Type ?u.24191
G
:
Type _: Type (?u.24191+1)
Type _
) [
DivisionCommMonoid: Type ?u.24194 β†’ Type ?u.24194
DivisionCommMonoid
G: Type ?u.24191
G
] :
G: Type ?u.24191
G
≃*
G: Type ?u.24191
G
:= {
Equiv.inv: (G : Type ?u.24309) β†’ [inst : InvolutiveInv G] β†’ Equiv.Perm G
Equiv.inv
G: Type ?u.24191
G
with toFun :=
Inv.inv: {Ξ± : Type ?u.24414} β†’ [self : Inv Ξ±] β†’ Ξ± β†’ Ξ±
Inv.inv
, invFun :=
Inv.inv: {Ξ± : Type ?u.24466} β†’ [self : Inv Ξ±] β†’ Ξ± β†’ Ξ±
Inv.inv
, map_mul' :=
mul_inv: βˆ€ {Ξ± : Type ?u.24508} [inst : DivisionCommMonoid Ξ±] (a b : Ξ±), (a * b)⁻¹ = a⁻¹ * b⁻¹
mul_inv
} #align mul_equiv.inv
MulEquiv.inv: (G : Type u_1) β†’ [inst : DivisionCommMonoid G] β†’ G ≃* G
MulEquiv.inv
#align add_equiv.neg
AddEquiv.neg: (G : Type u_1) β†’ [inst : SubtractionCommMonoid G] β†’ G ≃+ G
AddEquiv.neg
#align mul_equiv.inv_apply
MulEquiv.inv_apply: βˆ€ (G : Type u_1) [inst : DivisionCommMonoid G] (a : G), ↑(MulEquiv.inv G) a = a⁻¹
MulEquiv.inv_apply
#align add_equiv.neg_apply
AddEquiv.neg_apply: βˆ€ (G : Type u_1) [inst : SubtractionCommMonoid G] (a : G), ↑(AddEquiv.neg G) a = -a
AddEquiv.neg_apply
@[
to_additive: βˆ€ (G : Type u_1) [inst : SubtractionCommMonoid G], AddEquiv.symm (AddEquiv.neg G) = AddEquiv.neg G
to_additive
(attr := simp)] theorem
MulEquiv.inv_symm: βˆ€ (G : Type u_1) [inst : DivisionCommMonoid G], symm (inv G) = inv G
MulEquiv.inv_symm
(
G: Type ?u.24823
G
:
Type _: Type (?u.24823+1)
Type _
) [
DivisionCommMonoid: Type ?u.24826 β†’ Type ?u.24826
DivisionCommMonoid
G: Type ?u.24823
G
] : (
MulEquiv.inv: (G : Type ?u.24830) β†’ [inst : DivisionCommMonoid G] β†’ G ≃* G
MulEquiv.inv
G: Type ?u.24823
G
).
symm: {M : Type ?u.24837} β†’ {N : Type ?u.24836} β†’ [inst : Mul M] β†’ [inst_1 : Mul N] β†’ M ≃* N β†’ N ≃* M
symm
=
MulEquiv.inv: (G : Type ?u.24952) β†’ [inst : DivisionCommMonoid G] β†’ G ≃* G
MulEquiv.inv
G: Type ?u.24823
G
:=
rfl: βˆ€ {Ξ± : Sort ?u.24958} {a : Ξ±}, a = a
rfl
#align mul_equiv.inv_symm
MulEquiv.inv_symm: βˆ€ (G : Type u_1) [inst : DivisionCommMonoid G], MulEquiv.symm (MulEquiv.inv G) = MulEquiv.inv G
MulEquiv.inv_symm
-- porting note: no `add_equiv.neg_symm` in `mathlib3`