Documentation
Acmoi
.
Exercise3_1_2
Search
Google site search
return to top
source
Imports
Init
Mathlib.Data.Finset.Card
Mathlib.Data.Fintype.Basic
Mathlib.Data.Fintype.Prod
Imported by
sat_eq
unique_sol
paireq
proj1eq
proj2eq
reduce
amplify
source
def
sat_eq
(a :
ℕ
×
ℕ
)
(n :
ℕ
)
(x :
ℕ
×
ℕ
)
:
Prop
Equations
sat_eq
a
n
x
=
(
a
.1
*
x
.1
+
a
.2
*
x
.2
=
n
)
Instances For
source
def
unique_sol
(a :
ℕ
×
ℕ
)
(n :
ℕ
)
:
Prop
Equations
unique_sol
a
n
=
∃!
x
:
ℕ
×
ℕ
,
sat_eq
a
n
x
Instances For
source
theorem
paireq
(a :
ℕ
)
(b :
ℕ
)
(c :
ℕ
)
(d :
ℕ
)
(ha :
a
=
c
)
(hb :
b
=
d
)
:
(
a
,
b
)
=
(
c
,
d
)
source
theorem
proj1eq
{a :
ℕ
}
{b :
ℕ
}
{c :
ℕ
}
{d :
ℕ
}
(h :
(
a
,
b
)
=
(
c
,
d
)
)
:
a
=
c
source
theorem
proj2eq
{a :
ℕ
}
{b :
ℕ
}
{c :
ℕ
}
{d :
ℕ
}
(h :
(
a
,
b
)
=
(
c
,
d
)
)
:
b
=
d
source
theorem
reduce
(a :
ℕ
×
ℕ
)
(n :
ℕ
)
(x₀ :
ℕ
)
(u :
ℕ
)
(v :
ℕ
)
(original :
unique_sol
a
(
n
+
a
.2
*
v
)
∧
sat_eq
a
(
n
+
a
.2
*
v
)
(
x₀
,
u
+
v
)
)
:
unique_sol
a
n
source
theorem
amplify
(a :
ℕ
×
ℕ
)
(n :
ℕ
)
(x₀ :
ℕ
)
(u :
ℕ
)
(v :
ℕ
)
(u_pos :
0
<
u
)
(original :
unique_sol
a
n
∧
sat_eq
a
n
(
x₀
,
u
*
v
)
)
:
unique_sol
(
a
.1
,
a
.2
*
u
)
n