## Stream: maths

### Topic: Little lemma about subfields

#### Patrick Lutz (Aug 19 2020 at 07:26):

Is the following lemma in mathlib already in some form? If not, should I make a PR to add it?

import field_theory.subfield algebra.group_with_zero_power

lemma is_subfield.pow_mem {K : Type*} [field K] {a : K} {n : ℤ} {s : set K} [is_subfield s] (h : a ∈ s) : a ^ n ∈ s :=
begin
by_cases hn : n ≥ 0,
{   lift n to ℕ using hn,
exact is_submonoid.pow_mem h, },
{   rw [(show n = (-1)*(-n), by ring), fpow_mul, fpow_neg a, fpow_one],
lift -n to ℕ using (show -n ≥ 0, by linarith),
exact is_submonoid.pow_mem (is_subfield.inv_mem h), },
end


#### Patrick Lutz (Aug 19 2020 at 07:27):

Also is this the right stream in which to ask this kind of question?

#### Kenny Lau (Aug 19 2020 at 07:27):

I think we should bundle is_subfield

#### Kenny Lau (Aug 19 2020 at 07:28):

also, we use 2 spaces for indent

#### Patrick Lutz (Aug 19 2020 at 07:29):

Kenny Lau said:

also, we use 2 spaces for indent

Yeah, I know, but I'm too lazy to change it for zulip.

#### Patrick Lutz (Aug 19 2020 at 07:30):

Kenny Lau said:

I think we should bundle is_subfield

Yeah, Kevin Buzzard mentioned this in the Berkeley stream. But I want to have something like this in mathlib because we used it in proving the primitive element theorem and I don't want to wait to see if is_subfield gets bundled

#### Johan Commelin (Aug 19 2020 at 07:32):

@Patrick Lutz Small remark about the name, this should be fpow_mem

#### Johan Commelin (Aug 19 2020 at 07:33):

Also, it's true for subgroup_with_zero, but I'm scared of thinking that such an object will be brought into existence :see_no_evil:

#### Kenny Lau (Aug 19 2020 at 07:45):

Patrick Lutz said:

Kenny Lau said:

also, we use 2 spaces for indent

Yeah, I know, but I'm too lazy to change it for zulip.

you can edit the default setting

#### Kenny Lau (Aug 19 2020 at 07:46):

@Gabriel Ebner is the default setting 4 spaces for indent? if so, could you change it to 2 spaces?

#### Mario Carneiro (Aug 19 2020 at 07:47):

https://github.com/leanprover-community/mathlib/blob/master/.vscode/settings.json#L3

#### Kenny Lau (Aug 19 2020 at 07:48):

@Mario Carneiro then why do I still see people typing with 4 spaces?

#### Kenny Lau (Aug 19 2020 at 07:49):

maybe they're not on vscode...?

#### Patrick Lutz (Aug 19 2020 at 07:50):

Kenny Lau said:

maybe they're not on vscode...?

For reference I am using vscode and as far as I know I have never changed the indentation settings

#### Mario Carneiro (Aug 19 2020 at 07:50):

what are your indentation settings, according to vscode?

#### Mario Carneiro (Aug 19 2020 at 07:50):

ctrl-comma, type "indent" and see what is set for "user" and "workspace"

#### Mario Carneiro (Aug 19 2020 at 07:52):

the indentation setting is also visible in the bottom right on the status bar

#### Patrick Lutz (Aug 19 2020 at 07:52):

Default tab size is 4 and detect indentation is also on

#### Johan Commelin (Aug 19 2020 at 07:52):

Maybe they're working on another project?

#### Johan Commelin (Aug 19 2020 at 07:52):

Are you editing mathlib, or something that depends on mathlib?

#### Patrick Lutz (Aug 19 2020 at 07:52):

Johan Commelin said:

Maybe they're working on another project?

Yeah, I'm not on a branch of mathlib

#### Mario Carneiro (Aug 19 2020 at 07:52):

if it detects your indentation style, then that's a self fulfilling prophecy

lol

#### Patrick Lutz (Aug 19 2020 at 07:53):

It's also a project with some other people at Berkeley so I'm not sure whether the indentation in this particular file originated with me or someone else

#### Johan Commelin (Aug 19 2020 at 07:54):

I suggest you copy that file that Mario linked to

#### Mario Carneiro (Aug 19 2020 at 07:54):

you should set the indent to 2 space in "workspace" and put the file in your project

#### Johan Commelin (Aug 19 2020 at 07:54):

It will encourage everyone to follow mathlib's style

#### Mario Carneiro (Aug 19 2020 at 07:54):

which is equivalent to johan's suggestion

#### Patrick Lutz (Aug 19 2020 at 07:54):

Johan Commelin said:

Also, it's true for subgroup_with_zero, but I'm scared of thinking that such an object will be brought into existence :see_no_evil:

Should I make a PR with this version?

#### Johan Commelin (Aug 19 2020 at 07:55):

I really don't know if we should start thinking about bundled subgroups with zero

#### Johan Commelin (Aug 19 2020 at 07:55):

It sounds "off-topic"...

#### Johan Commelin (Aug 19 2020 at 07:55):

And because of bundling, subfields will not be subgroup_with_zero automatically

#### Patrick Lutz (Aug 19 2020 at 07:57):

So should I make a PR with the original version? Or wait for is_subfield to be bundled? Or something else?

#### Johan Commelin (Aug 19 2020 at 08:07):

@Kenny Lau I think you have a better feeling for how you want to proceed with field theory

#### Kenny Lau (Aug 19 2020 at 08:08):

as of now, is_subfield is only used in 5 files, so I don't really know what we should do

#### Johan Commelin (Aug 19 2020 at 08:31):

Sure, but we haven't started doing Galois theory in mathlib yet...

#### Johan Commelin (Aug 19 2020 at 08:32):

I guess that once we have Galois groups, we'll want to start using fixed_field quite a bit.

#### Johan Commelin (Aug 19 2020 at 08:33):

And if it is just a type, instead of a subfield, then fpow_mem will be painful

#### Johan Commelin (Aug 19 2020 at 08:33):

So there is a case for using substructures

#### Johan Commelin (Aug 19 2020 at 08:34):

Maybe we can do a typeclass predicate on bundled subrings? I guess that is very evil mixing of design choices.

#### Kevin Buzzard (Aug 19 2020 at 08:46):

Bundled subrings are essentially done in the bundled-subrings branch by the way, thanks to @Ashvni Narayanan There's just one non-mathlib-looking proof in there right now.

#### Ashvni Narayanan (Aug 19 2020 at 15:26):

Yeah, I am working on converting it into a term mode proof.

#### Patrick Massot (Aug 19 2020 at 15:32):

Why do you insist on having a proof term instead of a tactic proof?

#### Ashvni Narayanan (Aug 19 2020 at 15:36):

I am very happy to provide a tactic mode proof, if it is accepted.

#### Patrick Massot (Aug 19 2020 at 15:44):

Why wouldn't it be accepted? mathlib is full of tactics!

#### Ashvni Narayanan (Aug 19 2020 at 16:03):

The proof is quite long and winding. I thought term mode might be a more efficient way of doing it. However, I am finding it quite non-trivial to transform my proof.

Last updated: May 09 2021 at 10:11 UTC