checking my logic?

Stream: new members

[Lawrence Lin]

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]

nevermind. i realized my proof was circular. sorry

[Yaël Dillies]

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

is the answer to your question

[Lawrence Lin]

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

[Lawrence Lin]

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]

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]

thanks
let me keep trying

[Kevin Buzzard]

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

[Lawrence Lin]

oh..

[Lawrence Lin]

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

[Lawrence Lin]

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]

specifically "mul_geom_sum" doesn't work

[Ruben Van de Velde]

Note that zero is a natural in mathlib

[Lawrence Lin]

ou.

[Lawrence Lin]

how can we write "the positive integers" then?

[Riccardo Brasca]

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

[Lawrence Lin]

lemme see

[Riccardo Brasca]

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]

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

[Lawrence Lin]

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

[Lawrence Lin]

a as an integer, such that 0 < a

[Lawrence Lin]

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

[Lawrence Lin]

i believe i read something about natural subtraction defaulting

[Riccardo Brasca]

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

[Lawrence Lin]

yep! did that.

[Riccardo Brasca]

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]

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

[Lawrence Lin]

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]

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]

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

[Lawrence Lin]

thanks

[Floris van Doorn]

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]

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

[Floris van Doorn]

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

[Lawrence Lin]

they're not there. let me look again!

[Lawrence Lin]

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

[Floris van Doorn]

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

[Lawrence Lin]

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