# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: poly (a)eval and algebra maps

#### Moritz Firsching (Mar 11 2021 at 14:42):

I wonder if there are simpler ways of doing the following two lemmas of if there is some code for it which I overlooked:

```
import tactic
import ring_theory.power_series.basic
import number_theory.bernoulli
open power_series
open nat
open ring_hom
open polynomial (aeval)
variables {A : Type*} [comm_ring A] [algebra ℚ A]
lemma aux_eval (t : ℚ) (p: polynomial ℚ):
aeval (algebra_map ℚ A t) p = algebra_map ℚ A (p.eval t) :=
begin
dsimp [polynomial.aeval_def],
unfold polynomial.eval,
delta eval₂,
simp only [← ring_hom.map_sum, ring_hom.id_apply],
rw [finsupp.sum, finsupp.sum],
simp only [ring_hom.map_sum, ring_hom.map_pow, ring_hom.map_mul],
end
lemma aux_smul (q r : ℚ):
q • (algebra_map ℚ A) r = (algebra_map ℚ A) (q * r) :=
begin
simp only [ring_hom.map_mul],
rw [←algebra.smul_def, algebra.smul_def, algebra.commutes],
end
```

(see #6641 for context)

#### Eric Wieser (Mar 11 2021 at 14:50):

Can you make that a #mwe with imports?

#### Moritz Firsching (Mar 11 2021 at 14:55):

sure, done

#### Eric Wieser (Mar 11 2021 at 14:56):

```
lemma aux_eval {A : Type*} [semiring A] [algebra ℚ A] (t : ℚ) (p: polynomial ℚ):
aeval (algebra_map ℚ A t) p = algebra_map ℚ A (p.eval t) :=
begin
change aeval (algebra.of_id ℚ A t) p = _,
rw aeval_alg_hom,
refl,
end
```

#### Moritz Firsching (Mar 11 2021 at 14:59):

That's already much nicer!

#### Eric Wieser (Mar 11 2021 at 14:59):

Or as a one-line proof with some noise

```
section
-- this instance causes conflicts in the proof
local attribute [-instance] rat.algebra_rat
lemma aux_eval {A : Type*} [semiring A] [algebra ℚ A] (t : ℚ) (p: polynomial ℚ):
aeval (algebra_map ℚ A t) p = algebra_map ℚ A (p.eval t) :=
aeval_alg_hom_apply (algebra.of_id ℚ A) t p
end
```

The key observation here is that `algebra_map`

has a corresponding `alg_hom`

, which you can then use docs#polynomial.aeval_alg_hom_apply on

#### Moritz Firsching (Mar 11 2021 at 15:04):

Would it be useful to have that lemma somewhere as `aeval_map_eq_map_eval`

or should I use it in my proof only (I would probably not give it a name then, now that it is so short)?

#### Moritz Firsching (Mar 11 2021 at 15:06):

(deleted)

#### Eric Wieser (Mar 11 2021 at 15:08):

I think `aeval_algebra_map_apply`

would be a reasonable lemma with that definition

#### Eric Wieser (Mar 11 2021 at 15:08):

Except obviously generalizing over ` ℚ`

#### Eric Wieser (Mar 11 2021 at 15:09):

Which also removes the need for hiding the annoying instanec

#### Eric Wieser (Mar 11 2021 at 15:12):

second lemma is slightly shorter as:

```
lemma smul_algebra_map (q r : R) :
q • algebra_map R A r = algebra_map R A (q * r) :=
by rw [algebra.smul_def, ring_hom.map_mul]
```

#### Moritz Firsching (Mar 11 2021 at 19:32):

Thanks for the help, @Eric Wieser ! I have inlined aux_eval, not sure if this would be worthwhile to add to mathlib.

Made a separate pr for the first lemma 6649

Last updated: May 07 2021 at 22:14 UTC