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: port FieldTheory.SplittingField.Construction #4891

Closed
wants to merge 22 commits into from
Closed

[Merged by Bors] - feat: port FieldTheory.SplittingField.Construction #4891

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
22 commits
Select commit Hold shift + click to select a range
8fca37c
feat: port FieldTheory.SplittingField.Construction
ChrisHughes24 Jun 9, 2023
2388ba3
Initial file copy from mathport
ChrisHughes24 Jun 9, 2023
a0d78ca
automated fixes
ChrisHughes24 Jun 9, 2023
975919e
Prove existence of SplittingField
ChrisHughes24 Jun 9, 2023
45c686e
define SplittingField
ChrisHughes24 Jun 9, 2023
6a117ea
Prove IsScalarTower
ChrisHughes24 Jun 9, 2023
610c773
use rootSet
ChrisHughes24 Jun 10, 2023
9d9d027
fix build
ChrisHughes24 Jun 10, 2023
27583d1
small progress
ChrisHughes24 Jun 10, 2023
7737b38
add scalar tower instance in MvPolynomial
ChrisHughes24 Jun 10, 2023
5458307
finish modulo a few sorries
ChrisHughes24 Jun 10, 2023
3e78d8e
fix some yellow
ChrisHughes24 Jun 10, 2023
c3dd6ee
delete duplicate instance
ChrisHughes24 Jun 10, 2023
d030bd0
minor cleanup
Jun 12, 2023
084dda3
most of the field instance
Jun 12, 2023
c5d672e
Prove qsmul_eq_mul'
ChrisHughes24 Jun 12, 2023
c4a55f5
Update Mathlib/FieldTheory/SplittingField/IsSplittingField.lean
jcommelin Jun 13, 2023
ae712c9
adjoin_rootSet everywhere
jcommelin Jun 13, 2023
828cd04
and a bit more adjoin_rootSet
jcommelin Jun 13, 2023
0505a4d
minitweak
jcommelin Jun 13, 2023
022d6a6
fix final sorry
jcommelin Jun 13, 2023
90124bb
Merge branch 'master' into port/FieldTheory.SplittingField.Construction
eric-wieser Jun 14, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1741,6 +1741,7 @@ import Mathlib.FieldTheory.PerfectClosure
import Mathlib.FieldTheory.RatFunc
import Mathlib.FieldTheory.Separable
import Mathlib.FieldTheory.SeparableDegree
import Mathlib.FieldTheory.SplittingField.Construction
import Mathlib.FieldTheory.SplittingField.IsSplittingField
import Mathlib.FieldTheory.Subfield
import Mathlib.FieldTheory.Tower
Expand Down
8 changes: 8 additions & 0 deletions Mathlib/Data/MvPolynomial/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,6 +150,14 @@ instance isScalarTower' [CommSemiring R] [CommSemiring S₁] [Algebra R S₁] :
IsScalarTower.right
#align mv_polynomial.is_scalar_tower' MvPolynomial.isScalarTower'

--Porting note: new instance
instance isScalarTower_right [CommSemiring R] [CommSemiring S₁] [DistribSMul R S₁]
[IsScalarTower R S₁ S₁] : IsScalarTower R (MvPolynomial σ S₁) (MvPolynomial σ S₁) :=
⟨by
rintro x p q
dsimp [MvPolynomial] at p q ⊢
rw [smul_mul_assoc]⟩
Comment on lines +153 to +159
Copy link
Member

Choose a reason for hiding this comment

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

This is replaced in #5070


/-- If `R` is a subsingleton, then `MvPolynomial σ R` has a unique element -/
instance unique [CommSemiring R] [Subsingleton R] : Unique (MvPolynomial σ R) :=
AddMonoidAlgebra.unique
Expand Down