[WIP] Subrings subfields #261
Conversation
|
|
||
| variables [decidable_eq R] | ||
|
|
||
| noncomputable def polynomial.map {S : Type v} [comm_ring S] (f : S → cR) [is_ring_hom f] : polynomial S → polynomial cR := |
There was a problem hiding this comment.
I think these last 3 defs should be (re)moved.
There was a problem hiding this comment.
they should at least go into a different file - data.polynomial is a high end dependency. polynomial.map should definitely not be defined here at all though
field_theory/subfield.lean
Outdated
| zero_ne_one := begin apply (iff_false_left zero_ne_one).mp, simp, exact F, apply_instance, end, | ||
| mul_inv_cancel := assume ⟨a, _⟩, λ h, subtype.eq (mul_inv_cancel ((iff_false_left (not_not_intro h)).mp (begin dunfold ne, rw auto.not_not_eq, apply subtype.ext, end))), | ||
| inv_mul_cancel := assume ⟨a, _⟩, λ h, subtype.eq (inv_mul_cancel ((iff_false_left (not_not_intro h)).mp (begin dunfold ne, rw auto.not_not_eq, apply subtype.ext, end))), | ||
| mul_comm := assume ⟨a, _⟩ ⟨b, _⟩, subtype.eq (mul_comm a b),} |
There was a problem hiding this comment.
You should not have to prove all these axioms. Most of them are already given by the fact that it is a subring which gives you all the comm_ring axioms
| /- | ||
| Copyright (c) 2018 Johan Commelin. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Johan Commelin |
There was a problem hiding this comment.
I believe it was Johan
There was a problem hiding this comment.
I wrote this for the perfectoid project.
|
I'll work on this tonight. |
|
I think this has been superseded by #267, except for the I suggest we close this pull request, and @amswerdlow can send a new PR for those definitions. |
TO CONTRIBUTORS:
Make sure you have:
For reviewers: code review check list