# Zulip Chat Archive

## Stream: FLT-regular

### Topic: docstrings

#### Kevin Buzzard (Nov 09 2021 at 13:23):

Could someone PR a module docstring for `algebra.norm_eq_prod_embeddings`

? It's just hit mathlib. I want to use this theorem as an example of something on my blog and it would be good if someone added a nice docstring so I could point blog readers to the community API entry and it would look less intimidating than it does now.

#### Kevin Buzzard (Nov 09 2021 at 13:33):

How about

```
for L/K a finite separable extension of fields and E an algebraically closed extension of K, the norm (down to K) of an element x of L is equal to the product of the images of x over all the K-embeddings $latex \sigma$ of L into E.
```

am on mobile right now going to Cambridge :D

#### Chris Birkbeck (Nov 09 2021 at 13:40):

Sure I can try and do it .

#### Eric Rodriguez (Nov 09 2021 at 14:03):

#10242, for those following along here!

#### Chris Birkbeck (Nov 09 2021 at 14:04):

Ah yes, thank you!

#### Riccardo Brasca (Nov 09 2021 at 14:28):

Thanks! I wanted to do it before PRing it but I forgot

#### Riccardo Brasca (Nov 09 2021 at 17:13):

@Kevin Buzzard Depending on what you want to talk about, you may want to mention that in docs#algebra.norm_eq_prod_embeddings the assumption `is_scalar_tower K L E`

is not needed, and I realized this just because the linter told me so. (Here $L/K$ is the fields extension we are talking about, and mathematically we take an algebraically closed extension of $L$, that of course is also an algebraically closed extension of $K$.)

#### Riccardo Brasca (Nov 09 2021 at 17:25):

I just realized that `E`

is not even an `L`

-algebra :sweat_smile:

#### Kevin Buzzard (Nov 10 2021 at 00:04):

Yes, everything is consistent

#### Kevin Buzzard (Nov 09 2021 at 13:23):

Could someone PR a module docstring for `algebra.norm_eq_prod_embeddings`

? It's just hit mathlib. I want to use this theorem as an example of something on my blog and it would be good if someone added a nice docstring so I could point blog readers to the community API entry and it would look less intimidating than it does now.

#### Kevin Buzzard (Nov 09 2021 at 13:33):

How about

```
for L/K a finite separable extension of fields and E an algebraically closed extension of K, the norm (down to K) of an element x of L is equal to the product of the images of x over all the K-embeddings $latex \sigma$ of L into E.
```

am on mobile right now going to Cambridge :D

#### Chris Birkbeck (Nov 09 2021 at 13:40):

Sure I can try and do it .

#### Eric Rodriguez (Nov 09 2021 at 14:03):

#10242, for those following along here!

#### Chris Birkbeck (Nov 09 2021 at 14:04):

Ah yes, thank you!

#### Riccardo Brasca (Nov 09 2021 at 14:28):

Thanks! I wanted to do it before PRing it but I forgot

#### Riccardo Brasca (Nov 09 2021 at 17:13):

@Kevin Buzzard Depending on what you want to talk about, you may want to mention that in docs#algebra.norm_eq_prod_embeddings the assumption `is_scalar_tower K L E`

is not needed, and I realized this just because the linter told me so. (Here $L/K$ is the fields extension we are talking about, and mathematically we take an algebraically closed extension of $L$, that of course is also an algebraically closed extension of $K$.)

#### Riccardo Brasca (Nov 09 2021 at 17:25):

I just realized that `E`

is not even an `L`

-algebra :sweat_smile:

#### Kevin Buzzard (Nov 10 2021 at 00:04):

Yes, everything is consistent

Last updated: Dec 20 2023 at 11:08 UTC