Zulip Chat Archive

Stream: maths

Topic: subrings


view this post on Zulip Johan Commelin (Jun 07 2018 at 06:54):

/-- `S` is a subgroup: a set containing 1 and closed under multiplication, addition and and additive inverse. -/
class is_subring  (S : set R) : Prop := -- would like `extends is_add_subgroup`, but that class doesn't exist
(one_mem       : (1 : R)  S)
(mul_mem {x y} : x  S  y  S  x * y  S)
(add_mem {x y} : x  S  y  S  x + y  S)
(inv_mem {x}   : x  S  -x  S)

instance subtype.ring {S : set R} [is_subring S] : ring S := sorry

view this post on Zulip Johan Commelin (Jun 07 2018 at 06:55):

I think the route of defining is_add_subgroup will pay off in the end. Is this again one of those things where [to_additive] should help? The last time I tried that, it didn't work.

view this post on Zulip Johan Commelin (Jun 07 2018 at 07:08):

Ok, the easy way out: I'll extend is_submonoid. Even though it feels "unmathematical" to me.

view this post on Zulip Kevin Buzzard (Jun 07 2018 at 08:32):

A minimalist definition of subgroup is : non-empty and closed under lam x y,xy^{-1}. Is there any point using this minimalist definition? You could do the same with add_mem and inv_mem here. Does this save time or obfuscate? Or both?

view this post on Zulip Johan Commelin (Jun 07 2018 at 09:22):

I think it would be best if we could extend both is_submonoid and is_add_subgroup.

view this post on Zulip Scott Morrison (Jun 07 2018 at 10:39):

Regarding minimalist definitions (x * y^{-1}), I think it is best if the official definition is the bog standard definition, with no clever tricks or surprises. It's fine to then provide an alternative constructor which allows you to take advantage of shortcuts like this if you want them.

view this post on Zulip Scott Morrison (Jun 07 2018 at 10:40):

Until the constructions become seriously dire, I think it's best to optimise definitions to be usable (after you've constructed instances), rather than easy to satisfy.

view this post on Zulip Scott Morrison (Jun 07 2018 at 10:40):

(Of course actually redundant things should be lemmas.)

view this post on Zulip Johan Commelin (Jun 07 2018 at 15:22):

https://github.com/jcommelin/lean-perfectoid-spaces/tree/subring/src/for_mathlib

view this post on Zulip Johan Commelin (Jun 07 2018 at 15:22):

Here is a small start on subrings

view this post on Zulip Johan Commelin (Jun 08 2018 at 06:47):

Update: https://github.com/jcommelin/lean-perfectoid-spaces/blob/subring/src/for_mathlib/subring.lean

view this post on Zulip Johan Commelin (Jun 08 2018 at 06:47):

@Kevin Buzzard what do you think is the best strategy for integral elements?

view this post on Zulip Johan Commelin (Jun 08 2018 at 06:48):

Were univariate polynomials already there? Somewhere? Did Chris or Nicholas do this?

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:51):

I think lots of people did univariate polynomials

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:51):

but I don't know if anyone submitted a PR

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:51):

I think Kenny proved a universal property

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:52):

@Chris Hughes @Kenny Lau @Johannes Hölzl Did any of you PR a definition of a polynomial in 1 variable into mathlib?

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:53):

@Johan Commelin Note that for the definition of a perfectoid space it might be the case that one only has to formalise the definition, i.e. "I am a root of a monic poly with coefficients in the smaller ring"

view this post on Zulip Johan Commelin (Jun 08 2018 at 06:53):

Yes, that is what I am currently trying to do

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:53):

To prove integral closure is a ring will involve some Noetherian arguments

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:53):

but I am not sure this result is needed

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:53):

We need "I am a subring of R^o"

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 06:54):

but I am not sure we need "...and by the way R^o is a ring"

view this post on Zulip Johan Commelin (Jun 08 2018 at 06:54):

Right, we never take the closure (-; We only have stuff that already is a subring, and then prove it is closed

view this post on Zulip Johan Commelin (Jun 08 2018 at 06:54):

Oooh, what you are saying is different from what I was saying...

view this post on Zulip Johannes Hölzl (Jun 08 2018 at 08:58):

@Kevin Buzzard There are no univariate polynomials in mathlib or in a PR. I want to move the polynomials from Mason-Stother proof in July / August.

view this post on Zulip Chris Hughes (Jun 08 2018 at 10:59):

I will do that once I've done my project.

view this post on Zulip Johan Commelin (Jun 08 2018 at 11:21):

What is the best way to define the n-th power of an ideal?

view this post on Zulip Johan Commelin (Jun 08 2018 at 11:34):

Current proposal:

span {i |  x : multiset I, x.card = n  i = (x.map subtype.val).prod}

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:32):

I think Kenny did product of ideals so you could just define them recursively

view this post on Zulip Johannes Hölzl (Jun 08 2018 at 13:40):

Are Kenny's ideals a subtype parameterised by the ring? I guess they form a monoid? Then you could just write I ^ n?

view this post on Zulip Johan Commelin (Jun 08 2018 at 13:41):

But I has type set R. And there is some instance hanging around telling you that it is an ideal. So now Lean wants have_pow (set R) nat.

view this post on Zulip Johan Commelin (Jun 08 2018 at 13:41):

And that doesn't make sense.

view this post on Zulip Johan Commelin (Jun 08 2018 at 13:41):

But maybe I'm missing something.

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:58):

It doesn't make sense to a mathematician -- that's what you're missing.

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:58):

I think the idea in CS is that you just define I*J for I and J sets to be the ideal generated by the ij

view this post on Zulip Mario Carneiro (Jun 08 2018 at 13:58):

why not?

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:58):

it's the same math/CS thing

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:58):

it's just like dividing by zero

view this post on Zulip Mario Carneiro (Jun 08 2018 at 13:58):

Is that even a CS thing?

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:58):

yes

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:59):

nobody divides by zero except CS people

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:59):

oh

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:59):

maybe applied mathematicians do

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:59):

no not even them

view this post on Zulip Mario Carneiro (Jun 08 2018 at 13:59):

where's the division by zero

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:59):

they only do 0 / 0

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:59):

the "division by zero" is when you multiply two sets that are not ideals together

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:59):

when nobody in their right mind would do this

view this post on Zulip Mario Carneiro (Jun 08 2018 at 13:59):

presumably this is exactly what is meant by I^n

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 13:59):

Exactly

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:00):

The notion A*B for A,B sets is well defined even if they are not ideals

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 14:00):

It's just a different way of thinking about things. I know exactly why Johan is confused.

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 14:00):

Yes, well-defined and kind-of pointless

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:00):

but if you want to restrict to ideals, it makes no difference

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 14:00):

so we don't think of it

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 14:00):

exactly

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 14:00):

and then whenever you apply it, you are probably carrying around a proof that things are ideals

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:00):

not at all pointless, the notation is not limited to ring theory

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 14:00):

This is just another instance of this canonical disconnect

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 14:01):

we only define things where we need them

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 14:01):

you over-define and sift later

view this post on Zulip Kevin Buzzard (Jun 08 2018 at 14:01):

it's just cultural

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:01):

I'm certain I've seen A - B and A + B and other things as well with weirder sets than ideals

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:02):

i.e. "prove C + C = [0, 2] where C is the cantor set"

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:02):

0/0 is also well-defined. It is 57.

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:03):

but I'm not even stressing this domain of definition, define it on ideals if you want

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:03):

you can still define I^n that way

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:04):

And A * B for A B : set R has two definitions that make sense. (1) { a*b | a \in A, b \in B} or (2) span { a*b | a \in A, b \in B} sorry, I meant span { a*b | a \in span A, b \in span B}

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:04):

since I^(n+1) = I^n * I and I^0 = B and these are both ideals

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:04):

in ring theory you obviously need the second definition

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:04):

I would say that (1) is more natural. But for ideals you want (2)

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:05):

A question: using the set definition, is span (I*I*I) = span (span (I*I) * I)?

view this post on Zulip Kenny Lau (Jun 08 2018 at 14:05):

yes

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:06):

Anyway, Kevin, here is https://github.com/jcommelin/lean-perfectoid-spaces/tree/subring with is_integrally_closed up to some sorrys in mason-stother.

view this post on Zulip Kenny Lau (Jun 08 2018 at 14:06):

A subset B is trivial, to see that B subset A, suffices to show that span(I*I)*I subset I*I*I, and then it follows from distributivity

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:07):

Here's another CS-ism: instead of dealing with ideals, generalize to all sets by implicitly taking the span when you need to

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:08):

Ok, so we put a semiring structure on set R...

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:09):

One problem with doing this generally is that -A is taken in sets

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:10):

Hmm, there is no semiring structure actually. Because neg A is span (-A), and so neg neg A \ne A.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:11):

Unless A is an ideal... but that is a very crazy assumption. (-;

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:12):

I think the nice thing to do is to define a class ideals R, just as with opens X.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:12):

And then put the nice structure on ideals R.

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:12):

actually if you only want a semiring you don't need neg

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:13):

I don't think you have to worry about any cancellation

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:13):

but the distributive law fails I think

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:13):

Aah, you are right of course

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:14):

{1, 2}*({1} + {1}) = {2, 4}, {1, 2}*{1} + {1,2}*{1} = {2,3,4}

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:15):

No, your counterexample fails. Both sides are R.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:16):

And in fact, I think you get a semiring.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:16):

The output of + and * is always an ideal.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:17):

A + B is defined as span (span A +' span B), where +' is the stupid element-wise addition.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:17):

Analogously for *.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:18):

(I agree that my initial definition was wrong. But I had not learnt your CS-ism back then. So I didn't put in enough spans.)

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:21):

I think span (A +' B) should suffice?

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:22):

My observation is that elementwise addition is non-distributive (although it is associative and commutative if the underlying op is)

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:23):

Right, but you want that multiplication and addition of ideals is distributive.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:23):

That is a fact that will someday be in mathlib, I hope.

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:23):

So we tweak our definition, and throw in some extra spans.

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:26):

You don't need the extra spans though, the span in the upgraded addition is sufficient to fix the issues

view this post on Zulip Mario Carneiro (Jun 08 2018 at 14:27):

span (A *' span (B +' C)) = span (span (A *' B) +' span (A *' C))

view this post on Zulip Johan Commelin (Jun 08 2018 at 14:33):

Take A = R, B = {1} and C = {-1}. Then LHS = 0 while RHS = R.

view this post on Zulip Reid Barton (Jun 08 2018 at 16:34):

The main point here is that you should be writing (I : ideal R), not (I : set R) (h : is_ideal I) or whatever.

view this post on Zulip Johan Commelin (Jun 08 2018 at 16:49):

So why do we still write (R : Type) [ring R]? Shouldn't we write R : Ring and G : Group or something like that?

view this post on Zulip Johan Commelin (Jun 08 2018 at 16:51):

Or does the difference have to do with whether your class is a Prop?

view this post on Zulip Johan Commelin (Jun 08 2018 at 16:51):

So all the is_opens, is_ideals and is_subrings get gathered into classes opens, ideals, and subrings. But things like rings and groups shouldn't...

view this post on Zulip Reid Barton (Jun 08 2018 at 16:53):

I think in many cases you should also be writing R : Ring etc. Particularly in settings where the only thing you know about R is that it is a ring.

view this post on Zulip Reid Barton (Jun 08 2018 at 16:53):

R : Ring might be less convenient when dealing with specific objects. For examples, the real numbers are a ring but they are also a topological space, etc.

view this post on Zulip Johan Commelin (Jun 08 2018 at 16:55):

Right

view this post on Zulip Johan Commelin (Jun 08 2018 at 16:57):

@Reid Barton I think Mario said something along the lines that type inference and coercions don't work together.

view this post on Zulip Johan Commelin (Jun 08 2018 at 16:59):

So, suppose you have the following statement instance {R : Type} [ring R] (S: subrings R) : ring S. If you then want to prove instance {R : Type} [comm_ring R] (S: subrings R) : comm_ring S I think you run in to trouble, because now Lean needs to turn S into a Type and also infer that it is a ring.

view this post on Zulip Johan Commelin (Jun 08 2018 at 17:00):

And I couldn't just easily prove stuff.

view this post on Zulip Johan Commelin (Jun 08 2018 at 17:00):

(I don't have Lean here atm... so I can't reproduce the exact problem I ran into.

view this post on Zulip Ashvni Narayanan (Aug 01 2020 at 00:29):

lemma coe_bot : (( : subring R) : set R) = set.range (coe :   R) := (int.cast_ring_hom R).coe_set_range

Here, ⊥ is defined to be

instance : has_bot (subring R) := (int.cast_ring_hom R).set_range

The proof of the above lemma gives the error :

type mismatch at application
  (int.cast_ring_hom R).coe_set_range
term
  int.cast_ring_hom R
has type
   →+* R : Type u
but is expected to have type
  ?m_1 →+* ?m_2 : Type ?
Additional information:
c:\Users\ashvn\my_project\DVR\src\bundled_subrings_working.lean: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch at application
    (int.cast_ring_hom R).coe_set_range
  term
    int.cast_ring_hom R
  has type
     →+* R : Type u
  but is expected to have type
    ?m_1 →+* ?m_2 : Type ?

The lemma coe_set_range says:

@[simp] lemma coe_set_range : (f.set_range : set S) = set.range f := set.image_univ

I don't see why there is a type mismatch error occurs, since both \Z and R are rings. I also don't understand the long error.

view this post on Zulip Reid Barton (Aug 01 2020 at 00:33):

Try turning on set_option pp.all true?

view this post on Zulip Ashvni Narayanan (Aug 01 2020 at 00:44):

Gives the error:

type mismatch at application
  @ring_hom.coe_set_range.{?l_1} ?m_2 ?m_3 ?m_4 ?m_5 (@int.cast_ring_hom.{u} R _inst_1)
term
  @int.cast_ring_hom.{u} R _inst_1
has type
  @ring_hom.{0 u} int R int.semiring (@ring.to_semiring.{u} R _inst_1) : Type u
but is expected to have type
  @ring_hom.{?l_1 ?l_1} ?m_2 ?m_3 (@ring.to_semiring.{?l_1} ?m_2 ?m_4) (@ring.to_semiring.{?l_1} ?m_3 ?m_5) : Type ?l_1
Additional information:
c:\Users\ashvn\my_project\DVR\src\bundled_subrings_working.lean: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch at application
    @ring_hom.coe_set_range.{?l_1} ?m_2 ?m_3 ?m_4 ?m_5 (@int.cast_ring_hom.{u} R _inst_1)
  term
    @int.cast_ring_hom.{u} R _inst_1
  has type
    @ring_hom.{0 u} int R int.semiring (@ring.to_semiring.{u} R _inst_1) : Type u
  but is expected to have type
    @ring_hom.{?l_1 ?l_1} ?m_2 ?m_3 (@ring.to_semiring.{?l_1} ?m_2 ?m_4)
      (@ring.to_semiring.{?l_1} ?m_3 ?m_5) : Type ?l_1

It seems to me that the problem is that we have int.semiring instead of int.to_semiring?

view this post on Zulip Reid Barton (Aug 01 2020 at 00:52):

Is coe_set_range in mathlib?

view this post on Zulip Reid Barton (Aug 01 2020 at 00:52):

It looks like a universe issue

view this post on Zulip Reid Barton (Aug 01 2020 at 00:52):

@ring_hom.{0 u} versus @ring_hom.{?l_1 ?l_1}

view this post on Zulip Ashvni Narayanan (Aug 01 2020 at 00:52):

Actually, this is just a copy of

lemma coe_bot : (( : subsemiring R) : set R) = set.range (coe :   R) :=
(nat.cast_ring_hom R).coe_srange

for subrings, so this works for \N, but not for \Z (as a subring)

view this post on Zulip Ashvni Narayanan (Aug 01 2020 at 01:04):

Reid Barton said:

Is coe_set_range in mathlib?

No, the lemma I want to use is defined in the file.

view this post on Zulip Reid Barton (Aug 01 2020 at 01:18):

I would assume the variables are set up in a way that causes this universe issue.

view this post on Zulip Ashvni Narayanan (Aug 01 2020 at 01:23):

Changing

variable {R : Type u} [ring R]

to

variable {R : Type*} [ring R]

solved it, thank you!

view this post on Zulip Ashvni Narayanan (Aug 04 2020 at 15:47):

I have a ring R, and a list L : list(list R)) . I want to define a list M : list(list R)) such that

(list.map list.prod M).sum = - (list.map list.prod L).sum

I think this definition should do it :

    let M := list.map (list.map (has_neg )) L,

however, this gives an error

type mismatch at application
  list.map (list.map has_neg) L
term
  L
has type
  list (list R) : Type u_1
but is expected to have type
  list (list (Type ?)) : Type (?+1)

Any help is appreciated, thank you!

view this post on Zulip Adam Topaz (Aug 04 2020 at 15:51):

Is it because has_neg should be has_neg.neg?

view this post on Zulip Adam Topaz (Aug 04 2020 at 15:52):

Also, I don't think this would work, since the product of [-1,-2] is not the negative of the product of [1,2].

view this post on Zulip Adam Topaz (Aug 04 2020 at 15:53):

But it's possible I'm misunderstanding what you're trying to do here...

view this post on Zulip Adam Topaz (Aug 04 2020 at 16:17):

This is a difficult question, since list.prod evaluates the empty list to 1.

view this post on Zulip Adam Topaz (Aug 04 2020 at 16:18):

How you you define this for, say, the following list of lists: [[],[]]?

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 16:30):

(list.map list.prod L).sum when evaluated at [[1,2],[3,4]] is ([2,12]).sum which is 14. If you negate everything you still get 14.

view this post on Zulip Adam Topaz (Aug 04 2020 at 16:31):

Yeah, so it seems you want to only negate the head of each list, but then the empty lists cause issues.

view this post on Zulip Adam Topaz (Aug 04 2020 at 16:33):

I think you want to define a function like this:

import algebra

def helper {α : Type*} [ring α] : list α  list α
| [] := [-1]
| (a :: as) := -a :: as

and map using that.

view this post on Zulip Ashvni Narayanan (Aug 04 2020 at 21:57):

I defined

  let M := list.map (λ (b :list R), (list.cons (-1) b)) L,

and it seems to work. I believe it is equivalent to the definition you gave?
Thank you!

view this post on Zulip Adam Topaz (Aug 04 2020 at 21:57):

It's a bit different, but it also works.

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 21:58):

That should certainly work. What are you doing though?

view this post on Zulip Ashvni Narayanan (Aug 04 2020 at 22:01):

I was trying to prove this (got from the subsemiring file) :

lemma mem_closure_iff_exists_list {s : set R} {x} : x  closure s 
   L : list (list R), ( t  L,  y  t, y  s)  (L.map list.prod).sum = x :=

After struggling with the negation case for a while, I found this in the is_subring file :

theorem exists_list_of_mem_closure {s : set R} {x : R} (hx : x  closure s) :
  ( L : list (list R), ( t  L,  y  t, y  s  y = (-1:R))  (L.map list.prod).sum = x) :=

The proof is similar, so I am currently working the proof around.

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 22:02):

Then your suggestion looks perfect!

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 22:02):

Because -1 is in your ring

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 22:03):

The lemma as it stands without allowing -1 is false

view this post on Zulip Reid Barton (Aug 04 2020 at 22:03):

Yeah I'm confused

view this post on Zulip Ashvni Narayanan (Aug 04 2020 at 22:04):

Yes exactly, I realised that only after trying the negation case for very long

view this post on Zulip Reid Barton (Aug 04 2020 at 22:05):

Since exists_list_of_mem_closure already exists, what are you trying to prove? A corresponding statement for semirings? i.e. what is R?

view this post on Zulip Reid Barton (Aug 04 2020 at 22:07):

oh mem_closure_iff_exists_list also already exists, so now I'm doubly confused

view this post on Zulip Reid Barton (Aug 04 2020 at 22:07):

You're trying to prove mem_closure_iff_exists_list even though mathlib already has a proof?

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 22:09):

We're bundling subrings. It existed for is_subring.

view this post on Zulip Ashvni Narayanan (Aug 04 2020 at 22:12):

I am trying to adapt exists_list_of_mem_closure for bundled subrings, the definition of closure is somewhat different, and the existing proof breaks, because it uses something from deprecated.subgroups.

view this post on Zulip Reid Barton (Aug 04 2020 at 22:14):

I see


Last updated: May 06 2021 at 17:38 UTC