## Stream: maths

### Topic: how to use the pow_add theorem

#### Truong Nguyen (Sep 02 2018 at 19:10):

Dear Alls,
The pow_add theorem is as follow:

pow_add : ∀ (a : ?M_1) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ n

By why can't I prove the consequence theorem:

theorem th01 (a: ℕ ): ∀ m n:ℕ, a ^ (m + n) = (a ^ m) * (a ^ n) :=
begin
end

Here is the error that I got:

rewrite tactic failed, did not find instance of the pattern in the target expression
a ^ (?m_1 + ?m_2)
Thank you,

(deleted)

#### Chris Hughes (Sep 02 2018 at 19:14):

It's because you need to use nat.pow_add

#### Kenny Lau (Sep 02 2018 at 19:15):

because the ^ are different

#### Mario Carneiro (Sep 02 2018 at 19:15):

nat has a different instance for the power function, so it has its own theorems to go with it, like nat.pow_add

#### Chris Hughes (Sep 02 2018 at 19:15):

This is a very annoying feature of current lean. There are two definitions of pow on the naturals.

#### Mario Carneiro (Sep 02 2018 at 19:16):

If nat.pow_add was not proven, you could also use by simpa using pow_add a to prove it

#### Truong Nguyen (Sep 02 2018 at 19:21):

Dear Mario,
can you be more specific, what is by simpa using pow_add a.

#### Truong Nguyen (Sep 02 2018 at 19:24):

I changed to this:

theorem th01 (a: ℕ ): ∀ m n:ℕ, a ^ (m + n) = (a ^ m) * (a ^ n) :=
begin
end

But, it did not work neither.

#### Mario Carneiro (Sep 02 2018 at 19:26):

import algebra.group_power

theorem th01 (a m n : ℕ) : a ^ (m + n) = (a ^ m) * (a ^ n) :=
by simpa using pow_add a m n


#### Mario Carneiro (Sep 02 2018 at 19:27):

theorem th01 (a m n : ℕ) : a ^ (m + n) = (a ^ m) * (a ^ n) :=


#### Mario Carneiro (Sep 02 2018 at 19:27):

theorem th01 (a m n : ℕ) : a ^ (m + n) = (a ^ m) * (a ^ n) :=


#### Mario Carneiro (Sep 02 2018 at 19:28):

note that you need to have all the variables left of the colon for rw to work here

#### Truong Nguyen (Sep 02 2018 at 19:55):

Oh, great
Do you know how can I find the tutorial of using "simpa".

I have the following issue as well. I think it can be done in similar way.

How to use the theorem:
#check cardinal.mul_power
cardinal.mul_power : (?M_1 * ?M_2) ^ ?M_3 = ?M_1 ^ ?M_3 * ?M_2 ^ ?M_3

To prove that:
theorem th07 (a b n: \N): (a * b)^n = a ^n*b^n.

#### Mario Carneiro (Sep 02 2018 at 20:00):

That is an unrelated use of power; although it is possible it would be a weird way to prove that theorem for natural numbers

#### Mario Carneiro (Sep 02 2018 at 20:01):

the theorem itself is nat.mul_pow

#### Truong Nguyen (Sep 02 2018 at 20:04):

when I run the command:
#check nat.mul_pow

it gave me nothing.

#### Patrick Massot (Sep 02 2018 at 20:11):

import data.nat.basic

#### Truong Nguyen (Sep 03 2018 at 16:22):

Hello,
do you know where can I find the tutorial of using "simpa".

#### Patrick Massot (Sep 03 2018 at 16:23):

I think we don't have anything better than https://github.com/leanprover/mathlib/blob/master/docs/tactics.md#simpa

#### Truong Nguyen (Sep 03 2018 at 17:17):

Oh, thank you

Last updated: May 12 2021 at 08:14 UTC