mathlib3
[Merged by Bors] - refactor(field_theory/polynomial_galois_group): remove `open_locale classical`
#19184
Closed
Overview
Commits
1
Changes
View On GitHub

[Merged by Bors] - refactor(field_theory/polynomial_galois_group): remove `open_locale classical` #19184

eric-wieser wants to merge 1 commit into master from eric-wieser/more-classical
eric-wieser
eric-wieser refactor(field_theory/polynomial_galois_group): remove `open_locale c…
d708927b
eric-wieser eric-wieser added WIP
riccardobrasca
jcommelin
bors
github-actions github-actions added delegated
eric-wieser eric-wieser changed the title refactor(field_theory/polynomial_galois_group): remove `open_locale c… refactor(field_theory/polynomial_galois_group): remove `open_locale classical` 2 years ago
eric-wieser
bors
github-actions github-actions added ready-to-merge
riccardobrasca riccardobrasca removed WIP
riccardobrasca
ericrbg
ericrbg approved these changes on 2023-06-14
bors
bors bors changed the title refactor(field_theory/polynomial_galois_group): remove `open_locale classical` [Merged by Bors] - refactor(field_theory/polynomial_galois_group): remove `open_locale classical` 2 years ago
bors bors closed this 2 years ago
bors bors deleted the eric-wieser/more-classical branch 2 years ago

Login to write a write a comment.

Login via GitHub

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