Documentation
ModuleLocalProperties
.
MissingLemmas
.
Units
Search
Google site search
return to top
source
Imports
Init
Mathlib.Algebra.Group.Basic
Mathlib.Algebra.Group.Units.Defs
Imported by
unit_inv_eq_of_left'
unit_inv_eq_of_left
unit_inv_eq_of_right'
unit_inv_eq_of_right
unit_inv_eq_of_both
unit_inv_eq_iff
source
theorem
unit_inv_eq_of_left'
{M :
Type
u_1}
[
Monoid
M
]
{a :
M
}
{b :
M
}
{isunita :
IsUnit
a
}
(isunitb :
IsUnit
b
)
(left :
b
*
a
=
1
)
:
isunita
.unit
⁻¹
=
isunitb
.unit
source
theorem
unit_inv_eq_of_left
{M :
Type
u_1}
[
Monoid
M
]
{a :
M
}
{b :
M
}
{isunita :
IsUnit
a
}
(isunitb :
IsUnit
b
)
(left :
b
*
a
=
1
)
:
↑
isunita
.unit
⁻¹
=
b
source
theorem
unit_inv_eq_of_right'
{M :
Type
u_1}
[
Monoid
M
]
{a :
M
}
{b :
M
}
{isunita :
IsUnit
a
}
(isunitb :
IsUnit
b
)
(right :
a
*
b
=
1
)
:
isunita
.unit
⁻¹
=
isunitb
.unit
source
theorem
unit_inv_eq_of_right
{M :
Type
u_1}
[
Monoid
M
]
{a :
M
}
{b :
M
}
{isunita :
IsUnit
a
}
(isunitb :
IsUnit
b
)
(right :
a
*
b
=
1
)
:
↑
isunita
.unit
⁻¹
=
b
source
theorem
unit_inv_eq_of_both
{M :
Type
u_1}
[
Monoid
M
]
{a :
M
}
{b :
M
}
{isunita :
IsUnit
a
}
(left :
b
*
a
=
1
)
(right :
a
*
b
=
1
)
:
↑
isunita
.unit
⁻¹
=
b
source
theorem
unit_inv_eq_iff
{M :
Type
u_1}
[
Monoid
M
]
{a :
M
}
{b :
M
}
(h :
IsUnit
a
)
:
↑
h
.unit
⁻¹
=
b
↔
b
*
a
=
1
∧
a
*
b
=
1