Conversation
|
Something I noticed after upgrading the mathlib in my own project after #6500: All the lemmas that turned out to hold for rings and not just fields are actually in the |
|
Bolton, there's little point, I'm doing the whole file over again basically. I'll push what I have soon |
3c803e9 to
07dddc2
Compare
| · exact ⟨.inr ⟨x, h⟩, rfl⟩ | ||
|
|
||
| lemma sum_units_nonunits {α β : Type*} [Monoid α] [AddCommMonoid β] [Fintype α] [Fintype αˣ] | ||
| [Fintype <| nonunits α] (f : α → β) : |
There was a problem hiding this comment.
[lint-style] reported by reviewdog 🐶
| [Fintype <| nonunits α] (f : α → β) : | |
| [Fintype <| nonunits α] (f : α → β) : |
| variable (R) [Nontrivial R] | ||
|
|
||
| theorem X_pow_card_sub_X_natDegree_eq (hp : 1 < p) : | ||
| (X ^ p - X : R[X]).natDegree = p := |
There was a problem hiding this comment.
[lint-style] reported by reviewdog 🐶
| (X ^ p - X : R[X]).natDegree = p := | |
| (X ^ p - X : R[X]).natDegree = p := |
| variable [NoZeroDivisors R] | ||
|
|
||
| theorem Fintype.card_le_deg_mul_card_image_polynomial_eval [DecidableEq R] {p : R[X]} | ||
| (hp : 0 < p.degree) : Fintype.card R ≤ natDegree p * (univ.image (p.eval ·)).card := by |
There was a problem hiding this comment.
[lint-style] reported by reviewdog 🐶
| (hp : 0 < p.degree) : Fintype.card R ≤ natDegree p * (univ.image (p.eval ·)).card := by | |
| (hp : 0 < p.degree) : Fintype.card R ≤ natDegree p * (univ.image (p.eval ·)).card := by |
|
Just a thought: I saw you were making a new file - I have a few more lemmas to add along the lines of "sums of polynomials over subgroups" with the final goal of the univariate sumcheck lemma. If you are looking for a place to split out what goes in the new file, you could aim for selecting the lemmas which have the bigoperators in them. |
| variable (p : ℕ) [Fact p.Prime] [Algebra (ZMod p) K] | ||
| variable (p : ℕ) [Field K] [Fintype K] [Fact p.Prime] [Algebra (ZMod p) K] | ||
|
|
||
| theorem roots_X_pow_card_sub_X : roots (X ^ q - X : K[X]) = Finset.univ.val := by |
There was a problem hiding this comment.
Perhaps roots_X_pow_card_sub_X can be golfed with Lagrange.nodal_subgroup_eq_X_pow_card_sub_one
|
Interesting, I'll check that out. It's currently a bit stuck as I've been trying to use |
|
It is really impossible to do this because of Lean not wanting me to do stuff with the "non-canonical" instances; they are impossible to make defeq due to classically making up the |
As promised on #6500.
I have not even remotely finished this, this is mainly a reminder; if people want to help out feel free!
cc @BoltonBailey, as I was talking about on the thread.