Documentation
LeanCourse
.
MIL
.
C05_Elementary_Number_Theory
.
S01_Irrational_Roots
Search
Google site search
return to top
source
Imports
Init
LeanCourse.Common
Mathlib.Data.Nat.Factorization.Basic
Mathlib.Data.Nat.Prime.Basic
Imported by
even_of_even_sqr
factorization_mul'
factorization_pow'
Nat
.
Prime
.
factorization'
source
theorem
even_of_even_sqr
{m :
ℕ
}
(h :
2
∣
m
^
2
)
:
2
∣
m
source
theorem
factorization_mul'
{m :
ℕ
}
{n :
ℕ
}
(mnez :
m
≠
0
)
(nnez :
n
≠
0
)
(p :
ℕ
)
:
(
m
*
n
)
.factorization
p
=
m
.factorization
p
+
n
.factorization
p
source
theorem
factorization_pow'
(n :
ℕ
)
(k :
ℕ
)
(p :
ℕ
)
:
(
n
^
k
)
.factorization
p
=
k
*
n
.factorization
p
source
theorem
Nat
.
Prime
.
factorization'
{p :
ℕ
}
(prime_p :
Nat.Prime
p
)
:
p
.factorization
p
=
1