HepLean Documentation
Init
.
Data
.
Nat
.
Dvd
Search
Google site search
return to top
source
Imports
Init.Meta
Init.Data.Nat.Div
Imported by
Nat
.
dvd_refl
Nat
.
dvd_zero
Nat
.
dvd_mul_left
Nat
.
dvd_mul_right
Nat
.
dvd_trans
Nat
.
eq_zero_of_zero_dvd
Nat
.
zero_dvd
Nat
.
dvd_add
Nat
.
dvd_add_iff_right
Nat
.
dvd_add_iff_left
Nat
.
dvd_mod_iff
Nat
.
le_of_dvd
Nat
.
dvd_antisymm
Nat
.
pos_of_dvd_of_pos
Nat
.
one_dvd
Nat
.
eq_one_of_dvd_one
Nat
.
mod_eq_zero_of_dvd
Nat
.
dvd_of_mod_eq_zero
Nat
.
dvd_iff_mod_eq_zero
Nat
.
decidable_dvd
Nat
.
emod_pos_of_not_dvd
Nat
.
mul_div_cancel'
Nat
.
div_mul_cancel
Nat
.
mod_mod_of_dvd
Nat
.
dvd_of_mul_dvd_mul_left
Nat
.
dvd_of_mul_dvd_mul_right
Nat
.
dvd_sub
Nat
.
mul_dvd_mul
Nat
.
mul_dvd_mul_left
Nat
.
mul_dvd_mul_right
Nat
.
dvd_one
Nat
.
mul_div_assoc
source
theorem
Nat
.
dvd_refl
(a :
Nat
)
:
a
∣
a
source
theorem
Nat
.
dvd_zero
(a :
Nat
)
:
a
∣
0
source
theorem
Nat
.
dvd_mul_left
(a b :
Nat
)
:
a
∣
b
*
a
source
theorem
Nat
.
dvd_mul_right
(a b :
Nat
)
:
a
∣
a
*
b
source
theorem
Nat
.
dvd_trans
{a b c :
Nat
}
(h₁ :
a
∣
b
)
(h₂ :
b
∣
c
)
:
a
∣
c
source
theorem
Nat
.
eq_zero_of_zero_dvd
{a :
Nat
}
(h :
0
∣
a
)
:
a
=
0
source
@[simp]
theorem
Nat
.
zero_dvd
{n :
Nat
}
:
0
∣
n
↔
n
=
0
source
theorem
Nat
.
dvd_add
{a b c :
Nat
}
(h₁ :
a
∣
b
)
(h₂ :
a
∣
c
)
:
a
∣
b
+
c
source
theorem
Nat
.
dvd_add_iff_right
{k m n :
Nat
}
(h :
k
∣
m
)
:
k
∣
n
↔
k
∣
m
+
n
source
theorem
Nat
.
dvd_add_iff_left
{k m n :
Nat
}
(h :
k
∣
n
)
:
k
∣
m
↔
k
∣
m
+
n
source
theorem
Nat
.
dvd_mod_iff
{k m n :
Nat
}
(h :
k
∣
n
)
:
k
∣
m
%
n
↔
k
∣
m
source
theorem
Nat
.
le_of_dvd
{m n :
Nat
}
(h :
0
<
n
)
:
m
∣
n
→
m
≤
n
source
theorem
Nat
.
dvd_antisymm
{m n :
Nat
}
:
m
∣
n
→
n
∣
m
→
m
=
n
source
theorem
Nat
.
pos_of_dvd_of_pos
{m n :
Nat
}
(H1 :
m
∣
n
)
(H2 :
0
<
n
)
:
0
<
m
source
@[simp]
theorem
Nat
.
one_dvd
(n :
Nat
)
:
1
∣
n
source
theorem
Nat
.
eq_one_of_dvd_one
{n :
Nat
}
(H :
n
∣
1
)
:
n
=
1
source
theorem
Nat
.
mod_eq_zero_of_dvd
{m n :
Nat
}
(H :
m
∣
n
)
:
n
%
m
=
0
source
theorem
Nat
.
dvd_of_mod_eq_zero
{m n :
Nat
}
(H :
n
%
m
=
0
)
:
m
∣
n
source
theorem
Nat
.
dvd_iff_mod_eq_zero
{m n :
Nat
}
:
m
∣
n
↔
n
%
m
=
0
source
instance
Nat
.
decidable_dvd
:
DecidableRel
fun (
x1
x2
:
Nat
) =>
x1
∣
x2
Equations
x✝
.decidable_dvd
x
=
decidable_of_decidable_of_iff
⋯
source
theorem
Nat
.
emod_pos_of_not_dvd
{a b :
Nat
}
(h :
¬
a
∣
b
)
:
0
<
b
%
a
source
theorem
Nat
.
mul_div_cancel'
{n m :
Nat
}
(H :
n
∣
m
)
:
n
*
(
m
/
n
)
=
m
source
theorem
Nat
.
div_mul_cancel
{n m :
Nat
}
(H :
n
∣
m
)
:
m
/
n
*
n
=
m
source
@[simp]
theorem
Nat
.
mod_mod_of_dvd
{c b :
Nat
}
(a :
Nat
)
(h :
c
∣
b
)
:
a
%
b
%
c
=
a
%
c
source
theorem
Nat
.
dvd_of_mul_dvd_mul_left
{k m n :
Nat
}
(kpos :
0
<
k
)
(H :
k
*
m
∣
k
*
n
)
:
m
∣
n
source
theorem
Nat
.
dvd_of_mul_dvd_mul_right
{k m n :
Nat
}
(kpos :
0
<
k
)
(H :
m
*
k
∣
n
*
k
)
:
m
∣
n
source
theorem
Nat
.
dvd_sub
{k m n :
Nat
}
(H :
n
≤
m
)
(h₁ :
k
∣
m
)
(h₂ :
k
∣
n
)
:
k
∣
m
-
n
source
theorem
Nat
.
mul_dvd_mul
{a b c d :
Nat
}
:
a
∣
b
→
c
∣
d
→
a
*
c
∣
b
*
d
source
theorem
Nat
.
mul_dvd_mul_left
{b c :
Nat
}
(a :
Nat
)
(h :
b
∣
c
)
:
a
*
b
∣
a
*
c
source
theorem
Nat
.
mul_dvd_mul_right
{a b :
Nat
}
(h :
a
∣
b
)
(c :
Nat
)
:
a
*
c
∣
b
*
c
source
@[simp]
theorem
Nat
.
dvd_one
{n :
Nat
}
:
n
∣
1
↔
n
=
1
source
theorem
Nat
.
mul_div_assoc
{k n :
Nat
}
(m :
Nat
)
(H :
k
∣
n
)
:
m
*
n
/
k
=
m
*
(
n
/
k
)