Documentation
Acmoi
.
Exercise1_5
Search
Google site search
return to top
source
Imports
Init
Mathlib.Tactic
Mathlib.Combinatorics.SimpleGraph.Basic
Mathlib.Data.Vector.Basic
Imported by
decide_diophantine2_1
decide_diophantine2_2
example_1_59
source
theorem
decide_diophantine2_1
{a :
ℕ
}
{b :
ℕ
}
{n :
ℕ
}
{x :
ℕ
}
{y :
ℕ
}
(h :
a
*
x
+
b
*
y
=
n
)
(ha :
0
<
a
)
:
x
<
n
/
a
+
1
source
theorem
decide_diophantine2_2
{a :
ℕ
}
{b :
ℕ
}
{n :
ℕ
}
{x :
ℕ
}
{y :
ℕ
}
(g1 :
a
*
x
+
b
*
y
=
n
)
(ha :
0
<
a
)
(hb :
0
<
b
)
:
x
<
n
/
a
+
1
∧
y
<
n
/
b
+
1
source
instance
example_1_59
:
Decidable
(∀ (
x
y
:
ℕ
),
2
*
x
+
3
*
y
=
7
∧
(
x
>
0
→
y
>
0
)
↔
x
=
2
∧
y
=
1
)
Equations
example_1_59
=
decidable_of_iff
(∀ (
x
:
Fin
(
7
/
2
+
1
)
) (
y
:
Fin
(
7
/
3
+
1
)
),
2
*
↑
x
+
3
*
↑
y
=
7
∧
(
↑
x
>
0
→
↑
y
>
0
)
↔
↑
x
=
2
∧
↑
y
=
1
)
example_1_59.proof_1