how do I factor a polynomial in lean 3?

Stream: maths

[Lawrence Lin]

tldr, title. I'm trying to rewrite a^m - 1 as (a - 1)(a^m-1 + a^m-2 + a^m-3 + ... + a + 1).

[Lawrence Lin]

i can't seem to figure out how to tell lean to do that, though.

[Alex J. Best]

There is a lemma for this already in mathlib, the factor on the right is known as docs#geom_sum, and the lemma you want is docs#mul_geom_sum

[Lawrence Lin]

thanks!

[Lawrence Lin]

sorry for bothering here again, but i've encountered another problem. so...

import tactic
import algebra.group_with_zero.power
import algebra.big_operators.order
import algebra.big_operators.ring
import algebra.big_operators.intervals
import tactic.abel
import data.nat.parity

lemma mul_geom_sum [ring α] (x : α) (n : ℕ) :
(x - 1) * (∑ i in range n, x ^ i) = x ^ n - 1 :=
op_injective $ by simpa using geom_sum_mul (op x) n

example (a m n : ℕ) : (nat.gcd (a^m - 1) (a^n - 1)) = a^(nat.gcd m n) - 1 :=
begin
mul_geom_sum

end

i'm been trying to use this as my code, but when LEAN 3 seems to... not understand the lemma for mul_geom_sum.
ive copy pasted it from the docs hoping it'll work. is there something i'm doing wrong?

[Lawrence Lin]

nevermind, fixed it. i just downloaded the whole file and treated it as a library.

[Yakov Pechersky]

First of all, nat is not a ring. It is a semiring. Second, when you use a lemma in a tactic proof, you have to use it by using some tactic, not just saying it nakedly.

[Lawrence Lin]

oh i know, i just didn't type that bit out yet. thanks though

[Lawrence Lin]

i'm getting 59 errors in the geom_sum document for some reason, though. https://github.com/leanprover-community/mathlib/blob/08a8fd81a86c3e0b0a5f1da8baf4a519f6fa590c/src/algebra/geom_sum.lean#L184 the one over here.

[Lawrence Lin]

nvm fixed

[Scott Morrison]

Also, #backticks!