Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat(field_theory/separable): a separable polynomial is squarefree #5039

Closed
wants to merge 10 commits into from
Closed

[Merged by Bors] - feat(field_theory/separable): a separable polynomial is squarefree #5039

Changes from 1 commit
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
40ea44b
feat: (field_theory/separable): a separable polynomial is squarefree
riccardobrasca Nov 18, 2020
a523e9b
Update separable.lean
riccardobrasca Nov 18, 2020
379ab8a
Update separable.lean
riccardobrasca Nov 18, 2020
50fbfa4
Update src/field_theory/separable.lean
riccardobrasca Nov 18, 2020
2a4e6d9
Update src/field_theory/separable.lean
riccardobrasca Nov 18, 2020
d1836ea
Update separable.lean
riccardobrasca Nov 18, 2020
44a1c02
update number_theory/sum_two_squares
riccardobrasca Nov 18, 2020
235cfca
Update separable.lean
riccardobrasca Nov 18, 2020
a4af173
update field_theory/separable
riccardobrasca Nov 19, 2020
88f9f7b
Merge branch 'master' into square_freee_sep
riccardobrasca Nov 19, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 11 additions & 0 deletions src/field_theory/separable.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ import algebra.polynomial.big_operators
import field_theory.minimal_polynomial
import field_theory.splitting_field
import field_theory.tower
import algebra.squarefree
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I made algebra.squarefree a pretty big import. It might be preferable to put this lemma on the file algebra.squarefree instead to accomodate that, idk.
(This is still fine with me, just wanted to make sure a maintainer checks this)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah yes, that's also possible. Just let me know which one is better.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I feel like this is the more natural location. Maybe we can minimize the imports in algebra.squarefree in a future PR.


/-!

Expand Down Expand Up @@ -447,6 +448,16 @@ begin
exact_mod_cast (enat.add_one_le_of_lt hq)
end

lemma square_free_of_separable {p : polynomial F} (hp : p ≠ 0) (hsep : separable p) :
awainverse marked this conversation as resolved.
Show resolved Hide resolved
squarefree p :=
begin
apply (multiplicity.squarefree_iff_multiplicity_le_one p).2,
riccardobrasca marked this conversation as resolved.
Show resolved Hide resolved
intro f,
by_cases hunit : is_unit f,
{ exact or.inr hunit },
exact or.inl (multiplicity_le_one_of_seperable hunit hsep)
end

lemma root_multiplicity_le_one_of_seperable {p : polynomial F} (hp : p ≠ 0)
riccardobrasca marked this conversation as resolved.
Show resolved Hide resolved
(hsep : separable p) (x : F) : root_multiplicity x p ≤ 1 :=
begin
Expand Down