HepLean Documentation
Mathlib
.
Data
.
Int
.
Order
.
Units
Search
Google site search
return to top
source
Imports
Init
Mathlib.Algebra.Order.Ring.Abs
Imported by
Int
.
isUnit_iff_abs_eq
Int
.
isUnit_sq
Int
.
units_sq
Int
.
units_pow_two
Int
.
units_mul_self
Int
.
units_inv_eq_self
Int
.
units_div_eq_mul
Int
.
units_coe_mul_self
Int
.
neg_one_pow_ne_zero
Int
.
sq_eq_one_of_sq_lt_four
Int
.
sq_eq_one_of_sq_le_three
Int
.
units_pow_eq_pow_mod_two
Lemmas about units in
ℤ
, which interact with the order structure.
#
source
theorem
Int
.
isUnit_iff_abs_eq
{x :
ℤ
}
:
IsUnit
x
↔
|
x
|
=
1
source
theorem
Int
.
isUnit_sq
{a :
ℤ
}
(ha :
IsUnit
a
)
:
a
^
2
=
1
source
@[simp]
theorem
Int
.
units_sq
(u :
ℤ
ˣ
)
:
u
^
2
=
1
source
theorem
Int
.
units_pow_two
(u :
ℤ
ˣ
)
:
u
^
2
=
1
Alias
of
Int.units_sq
.
source
@[simp]
theorem
Int
.
units_mul_self
(u :
ℤ
ˣ
)
:
u
*
u
=
1
source
@[simp]
theorem
Int
.
units_inv_eq_self
(u :
ℤ
ˣ
)
:
u
⁻¹
=
u
source
theorem
Int
.
units_div_eq_mul
(u₁ u₂ :
ℤ
ˣ
)
:
u₁
/
u₂
=
u₁
*
u₂
source
@[simp]
theorem
Int
.
units_coe_mul_self
(u :
ℤ
ˣ
)
:
↑
u
*
↑
u
=
1
source
theorem
Int
.
neg_one_pow_ne_zero
{n :
ℕ
}
:
(-
1
)
^
n
≠
0
source
theorem
Int
.
sq_eq_one_of_sq_lt_four
{x :
ℤ
}
(h1 :
x
^
2
<
4
)
(h2 :
x
≠
0
)
:
x
^
2
=
1
source
theorem
Int
.
sq_eq_one_of_sq_le_three
{x :
ℤ
}
(h1 :
x
^
2
≤
3
)
(h2 :
x
≠
0
)
:
x
^
2
=
1
source
theorem
Int
.
units_pow_eq_pow_mod_two
(u :
ℤ
ˣ
)
(n :
ℕ
)
:
u
^
n
=
u
^
(
n
%
2
)