Zulip Chat Archive

Stream: maths

Topic: Little lemma about subfields


view this post on Zulip 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

view this post on Zulip Patrick Lutz (Aug 19 2020 at 07:27):

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

view this post on Zulip Kenny Lau (Aug 19 2020 at 07:27):

I think we should bundle is_subfield

view this post on Zulip Kenny Lau (Aug 19 2020 at 07:28):

also, we use 2 spaces for indent

view this post on Zulip 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.

view this post on 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

view this post on Zulip Johan Commelin (Aug 19 2020 at 07:32):

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

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Aug 19 2020 at 07:47):

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

view this post on Zulip Kenny Lau (Aug 19 2020 at 07:48):

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

view this post on Zulip Kenny Lau (Aug 19 2020 at 07:49):

maybe they're not on vscode...?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 19 2020 at 07:50):

what are your indentation settings, according to vscode?

view this post on Zulip Mario Carneiro (Aug 19 2020 at 07:50):

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

view this post on Zulip Mario Carneiro (Aug 19 2020 at 07:52):

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

view this post on Zulip Patrick Lutz (Aug 19 2020 at 07:52):

Default tab size is 4 and detect indentation is also on

view this post on Zulip Johan Commelin (Aug 19 2020 at 07:52):

Maybe they're working on another project?

view this post on Zulip Johan Commelin (Aug 19 2020 at 07:52):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 19 2020 at 07:52):

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

view this post on Zulip Patrick Lutz (Aug 19 2020 at 07:53):

lol

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 19 2020 at 07:54):

I suggest you copy that file that Mario linked to

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 19 2020 at 07:54):

It will encourage everyone to follow mathlib's style

view this post on Zulip Mario Carneiro (Aug 19 2020 at 07:54):

which is equivalent to johan's suggestion

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Aug 19 2020 at 07:55):

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

view this post on Zulip Johan Commelin (Aug 19 2020 at 07:55):

It sounds "off-topic"...

view this post on Zulip Johan Commelin (Aug 19 2020 at 07:55):

And because of bundling, subfields will not be subgroup_with_zero automatically

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 19 2020 at 08:31):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Aug 19 2020 at 08:33):

So there is a case for using substructures

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ashvni Narayanan (Aug 19 2020 at 15:26):

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

view this post on Zulip Patrick Massot (Aug 19 2020 at 15:32):

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

view this post on Zulip Ashvni Narayanan (Aug 19 2020 at 15:36):

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

view this post on Zulip Patrick Massot (Aug 19 2020 at 15:44):

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

view this post on Zulip 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