## Stream: new members

### Topic: checking my logic?

#### Lawrence Lin (Dec 14 2022 at 19:55):

hi! i'm trying to make sure that my logic with lean is correct.

import tactic
import algebra.geom_sum

lemma geom_sum_dvd (a : ℤ) (m n : ℕ) (h : m ∣ n) : (a^m - 1) ∣ (a^n - 1) :=
begin
rcases h with ⟨k, rfl⟩,
use geom_sum (a^m) k,
rw mul_geom_sum (a^m) _,
rw pow_mul,
end

example (a : ℤ) (m n : ℕ) : ↑(int.gcd (a^m - 1) (a^n - 1) : ℤ) = a^(nat.gcd m n) - 1 :=
begin
have H1 := geom_sum_dvd (a) (nat.gcd m n) (m) (nat.gcd_dvd_left m n),
have H2 := geom_sum_dvd (a) (nat.gcd m n) (n) (nat.gcd_dvd_right m n),
sorry,
end


my goal right now is i want to show (a^m - 1) / (a^gcd(m, n) - 1) and (a^n - 1) / (a^gcd(m, n) - 1) has a gcd of 1.
how do i write a new statement inside of my example?

#### Lawrence Lin (Dec 14 2022 at 19:57):

nevermind. i realized my proof was circular. sorry

#### Yaël Dillies (Dec 14 2022 at 19:57):

  have : gcd ((a^m - 1) / (a^gcd(m, n) - 1)) ((a^n - 1) / (a^gcd(m, n) - 1)),
{ sorry }


#### Lawrence Lin (Dec 14 2022 at 19:59):

thanks! how do i define a new variable in lean btw?

#### Lawrence Lin (Dec 14 2022 at 20:00):

like, i want to say:
let k = a^gcd(m, n)

but

variable k = a^(nat.gcd m n)


isn't working

#### Yaël Dillies (Dec 14 2022 at 20:01):

You can do set k := a ^ m.gcd n with hk (or let k := a ^ m.gcd n, which will probably be less practical).

#### Lawrence Lin (Dec 14 2022 at 20:03):

thanks
let me keep trying

#### Kevin Buzzard (Dec 14 2022 at 20:06):

Is this definitely true e.g. when a=0?

oh..

#### Lawrence Lin (Dec 14 2022 at 20:08):

i'm sorry, it should be naturals a, m, n

#### Lawrence Lin (Dec 14 2022 at 20:12):

lemma geom_sum_dvd (a m n : ℕ) (h : m ∣ n) : (a^m - 1) ∣ (a^n - 1) :=
begin
rcases h with ⟨k, rfl⟩,
use geom_sum (a^m) k,
rw mul_geom_sum (a^m) _,
rw pow_mul,
end

example (a m n : ℕ) : (nat.gcd (a^m - 1) (a^n - 1)) = a^(nat.gcd m n) - 1 :=
begin
have H1 := geom_sum_dvd (a) (nat.gcd m n) (m) (nat.gcd_dvd_left m n),
have H2 := geom_sum_dvd (a) (nat.gcd m n) (n) (nat.gcd_dvd_right m n),

set k := a^(nat.gcd m n) with hk,
rw ← mul_geom_sum a k, /- ignore this -/

sorry,
end


looks like this broke now. aw..

#### Lawrence Lin (Dec 14 2022 at 20:13):

specifically "mul_geom_sum" doesn't work

#### Ruben Van de Velde (Dec 14 2022 at 20:13):

Note that zero is a natural in mathlib

ou.

#### Lawrence Lin (Dec 14 2022 at 20:13):

how can we write "the positive integers" then?

#### Riccardo Brasca (Dec 14 2022 at 20:24):

We have the type ℕ+ of positive integers, but the API is less developed. You can just use (n : ℕ) (hpos : 0 < n)

lemme see

#### Riccardo Brasca (Dec 14 2022 at 20:25):

I mean, the two approaches are completely equivalent, but the second will save you to go through some coercion (meaning having to tell Lean that a positive natural is also a natural).

#### Kevin Buzzard (Dec 14 2022 at 20:26):

Are you sure that's true? Now you have natural subtraction.

#### Lawrence Lin (Dec 14 2022 at 20:26):

i think i'll keep a as an integer for now

#### Lawrence Lin (Dec 14 2022 at 20:27):

a as an integer, such that 0 < a

#### Lawrence Lin (Dec 14 2022 at 20:27):

so basically "nonnegative integers" instead of "nonnegative naturals"... if that makes a difference in lean

#### Riccardo Brasca (Dec 14 2022 at 20:34):

If you want to use integers than you have to write (n : ℤ ).

yep! did that.

#### Riccardo Brasca (Dec 14 2022 at 20:35):

Note that (n : ℤ) (hn : 0 < n), (n : ℕ) (hn : 0 < n) and (n : ℕ+) are not the same thing in Lean, even if mathematically there is (essentially) no difference.

#### Lawrence Lin (Dec 14 2022 at 20:37):

yea!
it's because of naturals subtraction, right?

#### Lawrence Lin (Dec 14 2022 at 20:37):

oh wait.. i thnk i know how to prove this now. let's use the euclidean algorithm! i heard that was built into lean already
do you know how i can find the doucmentation for that?

#### Floris van Doorn (Dec 14 2022 at 20:54):

https://leanprover-community.github.io/mathlib-overview.html and https://leanprover-community.github.io/undergrad.html are good pages to find things that are named in mathematics

#### Floris van Doorn (Dec 14 2022 at 20:55):

many times you want a simple lemma that does not have a name in mathematics, e.g. gcd n 0 = n. In that case I recommend searching in on https://leanprover-community.github.io/mathlib_docs/ for e.g. gcd_zero

thanks

#### Floris van Doorn (Dec 14 2022 at 20:56):

and slowly you'll get a sense of the naming scheme used in mathlib, which is very important to locate results you want to use.

#### Lawrence Lin (Dec 14 2022 at 20:57):

looks like i'll have to make the euclidean algorithm myself. hmmm

#### Floris van Doorn (Dec 14 2022 at 20:57):

nope, search for Euclid's algorithm on one of the two pages I linked

#### Lawrence Lin (Dec 14 2022 at 20:58):

they're not there. let me look again!

#### Lawrence Lin (Dec 14 2022 at 20:58):

ohhh, it's euclid's' algorithm with 2 apostrophes. got it

#### Floris van Doorn (Dec 14 2022 at 20:59):

I guess that is a bit tricky. I myself just searched for Euclid and found them that way :-)

#### Lawrence Lin (Dec 14 2022 at 20:59):

i see c: i saw things that were unrelated so i skimmed too fast, haha

Last updated: Dec 20 2023 at 11:08 UTC