Documentation
Mathlib
.
LinearAlgebra
.
SModEq
.
Pow
Search
return to top
source
Imports
Init
Mathlib.Algebra.CharP.Lemmas
Mathlib.LinearAlgebra.SModEq.Basic
Mathlib.RingTheory.Ideal.Operations
Imported by
SModEq
.
pow_mul_of_le
SModEq
.
pow_add_one
SModEq
.
pow_pow_add_one
Lemmas about SModEq related to powers
#
source
theorem
SModEq
.
pow_mul_of_le
{
R
:
Type
u_1}
[
CommRing
R
]
{
I
J
:
Ideal
R
}
{
p
:
ℕ
}
(
hpI
:
↑
p
∈
I
)
{
x
y
:
R
}
(
h
:
x
≡
y
[SMOD
J
]
)
(
hJI
:
J
≤
I
)
:
x
^
p
≡
y
^
p
[SMOD
J
*
I
]
source
theorem
SModEq
.
pow_add_one
{
R
:
Type
u_1}
[
CommRing
R
]
{
I
:
Ideal
R
}
{
p
:
ℕ
}
(
hpI
:
↑
p
∈
I
)
{
x
y
:
R
}
{
m
:
ℕ
}
(
hm
:
m
≠
0
)
(
h
:
x
≡
y
[SMOD
I
^
m
]
)
:
x
^
p
≡
y
^
p
[SMOD
I
^
(
m
+
1
)
]
source
theorem
SModEq
.
pow_pow_add_one
{
R
:
Type
u_1}
[
CommRing
R
]
{
I
:
Ideal
R
}
{
p
:
ℕ
}
(
hpI
:
↑
p
∈
I
)
{
x
y
:
R
}
(
h
:
x
≡
y
[SMOD
I
]
)
(
m
:
ℕ
)
:
x
^
p
^
m
≡
y
^
p
^
m
[SMOD
I
^
(
m
+
1
)
]