subtype instance

Stream: maths

[Patrick Massot]

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]

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

[Patrick Massot]

Oh, sorry I misunderstood.

[Patrick Massot]

but actually the file header is correct

[Andreas Swerdlow]

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

[Patrick Massot]

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]

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

[Scott Morrison]

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.