[Merged by Bors] - chore(field_theory/separable): generalize theorems #10337
Conversation
| by_contra hzero, | ||
| exact hdiv ((zmod.nat_coe_zmod_eq_zero_iff_dvd n p).1 hzero) }, | ||
| { exact (separable_X_pow_sub_C 1 | ||
| (λ h, hdiv $ (zmod.nat_coe_zmod_eq_zero_iff_dvd n p).1 h) one_ne_zero).squarefree }, |
There was a problem hiding this comment.
There is some weird issues that happen if you leave in the original proof but with .squarefree instead; I'm happy to revert this lemma deletion if you guys think this is worth it.
ericrbg
added
the
awaiting-CI
| @@ -195,7 +195,8 @@ begin | |||
| letI := classical.dec_eq E, | |||
| rw [norm_gen_eq_prod_roots pb hE, fintype.prod_equiv pb.lift_equiv', finset.prod_mem_multiset, | |||
| finset.prod_eq_multiset_prod, multiset.to_finset_val, | |||
| multiset.erase_dup_eq_self.mpr (nodup_roots ((separable_map _).mpr hfx)), multiset.map_id], | |||
| multiset.erase_dup_eq_self.mpr, multiset.map_id], | |||
| { exact nodup_roots ((separable_map _).mpr hfx) }, | |||
There was a problem hiding this comment.
i'm not sure why this is necessary, nodup_roots only changed from field K to comm_ring R, is_domain R!
github-actions
bot
removed
the
awaiting-CI
ericrbg
added
the
awaiting-review
| variable [hp : fact p.prime] | ||
| include hp | ||
|
|
||
| theorem expand_char (f : polynomial R) : map (frobenius R p) (expand R p f) = f ^ p := |
There was a problem hiding this comment.
Shouldn't this be called map_frobenius_expand? Or are you just moving this lemma?
There was a problem hiding this comment.
all the lemmas here (apart from separable_of_subsingleton) were just moved; I'm still happy to rename this, though; it seems a better name
There was a problem hiding this comment.
I think we should go through the whole file in a separate PR since there's some suboptimal naming throughout e.g. the pattern whatever_of_separable to separable.whatever.
jcommelin
added
awaiting-author
Co-authored-by: Johan Commelin <johan@commelin.net>
ericrbg
added
awaiting-review
github-actions
bot
added
the
merge-conflict
github-actions
bot
removed
the
merge-conflict
|
✌️ ericrbg can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors r+ |
Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>
I touched a lot of adjacent files to fix proofs that got modified, sorry! Also, something that I wonder is whether it is worth making some of the
char_presults aboutring_char Rinstead; another thing I worry about is the fact I turned quite a fewfact p.primearguments intop≠0; in most cases, this was a direct improvement, but when it's char p, we already havep≠0↔p.prime, and so we lose some convenience by giving up typeclasses there. Is it worth reverting that? Or making primed versions that take the fact?