Little lemma about subfields

Stream: maths

[Patrick Lutz]

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]

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

[Kenny Lau]

I think we should bundle is_subfield

[Kenny Lau]

also, we use 2 spaces for indent

[Patrick Lutz]

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]

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]

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

[Johan Commelin]

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]

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]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

maybe they're not on vscode...?

[Patrick Lutz]

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]

what are your indentation settings, according to vscode?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Lutz]

Default tab size is 4 and detect indentation is also on

[Johan Commelin]

Maybe they're working on another project?

[Johan Commelin]

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

[Patrick Lutz]

Johan Commelin said:

Maybe they're working on another project?

Yeah, I'm not on a branch of mathlib

[Mario Carneiro]

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

[Patrick Lutz]

lol

[Patrick Lutz]

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]

I suggest you copy that file that Mario linked to

[Mario Carneiro]

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

[Johan Commelin]

It will encourage everyone to follow mathlib's style

[Mario Carneiro]

which is equivalent to johan's suggestion

[Patrick Lutz]

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]

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

[Johan Commelin]

It sounds "off-topic"...

[Johan Commelin]

And because of bundling, subfields will not be subgroup_with_zero automatically

[Patrick Lutz]

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

[Johan Commelin]

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

[Kenny Lau]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

So there is a case for using substructures

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Patrick Massot]

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

[Ashvni Narayanan]

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

[Patrick Massot]

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

[Ashvni Narayanan]

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.