## Stream: maths

### Topic: subtype instance

#### Patrick Massot (Aug 19 2018 at 20:29):

In PR #261 coming from the perfectoid project, Johan defined subrings and subfields and proved they are rings and fields respectively. The proofs were of course extremely similar to the case of monoids and groups. So I exploited^Wencouraged Simon to write a new tactic built on top of refine_struct in the spirit of pi_instance. The result is #267. Of course any comment is welcome, but I'd be particularly interested in trying to answer question about how this tactic works, since I managed to fool myself into believing I mostly understand it and should write a tutorial about it.

#### Johan Commelin (Aug 20 2018 at 05:24):

Just for the record, I only did the parts on subrings. @Andreas Swerdlow deserves all credit for the work on subfields.

#### Patrick Massot (Aug 20 2018 at 09:27):

Oh, sorry I misunderstood.

#### Patrick Massot (Aug 20 2018 at 09:36):

but actually the file header is correct

#### Andreas Swerdlow (Aug 20 2018 at 09:41):

@Simon Hudon deserves credit for the newest version of subfield.lean

#### Patrick Massot (Aug 20 2018 at 09:52):

I'm not sure we have a very clear attribution policy in mathlib. But it's a very small file in any case. The main thing Simon added is the tactic, which is not in this file

#### Simon Hudon (Aug 20 2018 at 16:54):

I think we can mention more names than just mine. That was a team effort.

#### Scott Morrison (Aug 22 2018 at 05:25):

I think a good policy with attribution on files is to just gradually add more names: even if someone does a complete rewrite of a file, keep the old names as well. We have git blame and git history generally if the details ever matter.

Last updated: May 06 2021 at 17:38 UTC