mathlib3
[Merged by Bors] - chore(field_theory/splitting_field): split file
#19154
Closed
Overview
Commits
7
Changes
View On GitHub

[Merged by Bors] - chore(field_theory/splitting_field): split file #19154

riccardobrasca wants to merge 7 commits into master from RB/is_splitting_field
riccardobrasca
riccardobrasca first try
5ff34a87
riccardobrasca riccardobrasca added WIP
riccardobrasca header
0e94d09a
riccardobrasca move
3dd5e80d
riccardobrasca move a lemma
c2b3ab73
riccardobrasca fix build
0cc38e21
riccardobrasca fix also this
1918dc6d
riccardobrasca riccardobrasca changed the title first try chore(field_theory/splitting_field): split file 3 years ago
riccardobrasca another one
01e92e88
riccardobrasca riccardobrasca removed WIP
riccardobrasca riccardobrasca added awaiting-review
jcommelin
jcommelin approved these changes on 2023-06-05
leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge
leanprover-community-bot-assistant leanprover-community-bot-assistant removed awaiting-review
bors
bors bors changed the title chore(field_theory/splitting_field): split file [Merged by Bors] - chore(field_theory/splitting_field): split file 3 years ago
bors bors closed this 3 years ago
bors bors deleted the RB/is_splitting_field branch 3 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum