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.Ratfunc #4293

Closed
wants to merge 30 commits into from
Closed

[Merged by Bors] - feat: port FieldTheory.Ratfunc #4293

Show file tree
Hide file tree
Changes from 24 commits
Commits
Show all changes
30 commits
Select commit Hold shift + click to select a range
56f74eb
feat: port FieldTheory.Ratfunc
adomani May 24, 2023
2169692
Initial file copy from mathport
adomani May 24, 2023
c727928
automated fixes
adomani May 24, 2023
9a2a76a
A few fixes, until tactic stuff
adomani May 24, 2023
bf53876
use theorem instead of irreducible_def
ChrisHughes24 May 24, 2023
37e5942
Some fixes
Ruben-VandeVelde May 24, 2023
5f90e0e
Small steps forward
adomani May 24, 2023
e7f3d99
Many fixes
Vierkantor May 25, 2023
dfe7367
Merge branch 'port/FieldTheory.Ratfunc' of github.com:leanprover-comm…
adomani May 25, 2023
def7d57
More progress
adomani May 25, 2023
b1ba85f
Many fixes!
adomani May 25, 2023
aafc671
Lint
adomani May 25, 2023
1c4d756
Lint again
adomani May 25, 2023
2eb76f4
Fix liftRingHom
Vierkantor May 25, 2023
e9854c1
Replace frac_tac with explicit proof
Vierkantor May 25, 2023
1691624
Fix `num_div_denom` (use the right induction principle)
Vierkantor May 25, 2023
5cb16c1
A few `norm_cast` fixes
Vierkantor May 25, 2023
0456cd9
Fix the coercion to laurent series not being a `@[coe]`
Vierkantor May 25, 2023
9707e63
Fix apart from the `@[norm_cast]` error
Vierkantor May 25, 2023
0dfcbb2
Lint fix
Vierkantor May 25, 2023
4c84416
Document `section CommRing` vs `include/omit`
adomani May 25, 2023
b6ab151
Remove sectioning that is no longer needed.
adomani May 25, 2023
46f67e2
Remove explicit names for typeclass assumptions
adomani May 25, 2023
cffd941
Porting note: new type instead of `omit/include`.
adomani May 25, 2023
ab92298
Doc improvements
Vierkantor May 25, 2023
d823d83
Fix names
Vierkantor May 25, 2023
a53683b
Rename `Ratfunc` to `RatFunc`
Vierkantor May 25, 2023
bc77c39
auto: naming
Vierkantor May 25, 2023
05c4406
Fix overlong line
Vierkantor May 25, 2023
c58178d
Fix overzealous renames in #align
Vierkantor May 25, 2023
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
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 @@ -1426,6 +1426,7 @@ import Mathlib.FieldTheory.Minpoly.Basic
import Mathlib.FieldTheory.Minpoly.Field
import Mathlib.FieldTheory.MvPolynomial
import Mathlib.FieldTheory.PerfectClosure
import Mathlib.FieldTheory.Ratfunc
import Mathlib.FieldTheory.Separable
import Mathlib.FieldTheory.Subfield
import Mathlib.FieldTheory.Tower
Expand Down
Loading
Loading