mathlib3
[Merged by Bors] - chore(field_theory.finite.galois_field, number_theory.cyclotomic.basic): make splitting_field.algebra' an instance again
#19191

Closed

[Merged by Bors] - chore(field_theory.finite.galois_field, number_theory.cyclotomic.basic): make splitting_field.algebra' an instance again #19191

riccardobrasca wants to merge 2 commits into master from RB/splitting_field.algebra

this is useless

4232b76e

riccardobrasca added easy

riccardobrasca added awaiting-review

riccardobrasca removed awaiting-review

riccardobrasca added awaiting-CI

github-actions added delegated

let's try this

903d9217

riccardobrasca changed the title ~~chore(number_theory.cyclotomic.basic): remove useless local attribute~~ chore(field_theory.finite.galois_field & number_theory.cyclotomic.basic): remove useless local attribute 2 years ago

riccardobrasca changed the title ~~chore(field_theory.finite.galois_field & number_theory.cyclotomic.basic): remove useless local attribute~~ chore(field_theory.finite.galois_field, number_theory.cyclotomic.basic): remove useless local attribute 2 years ago

Vierkantor requested a review from

Vierkantor 2 years ago

Vierkantor changed the title ~~chore(field_theory.finite.galois_field, number_theory.cyclotomic.basic): remove useless local attribute~~ chore(field_theory.finite.galois_field, number_theory.cyclotomic.basic): make splitting_field.algebra' an instance again 2 years ago

Vierkantor approved these changes on 2023-06-15

riccardobrasca removed awaiting-CI

github-actions added ready-to-merge

bors changed the title ~~chore(field_theory.finite.galois_field, number_theory.cyclotomic.basic): make splitting_field.algebra' an instance again~~ [Merged by Bors] - chore(field_theory.finite.galois_field, number_theory.cyclotomic.basic): make splitting_field.algebra' an instance again 2 years ago

bors closed this 2 years ago

bors deleted the RB/splitting_field.algebra branch 2 years ago

Reviewers

Vierkantor

Assignees

No one assigned

Labels

ready-to-merge easy delegated

Milestone

No milestone

mathlib3 [Merged by Bors] - chore(field_theory.finite.galois_field, number_theory.cyclotomic.basic): make splitting_field.algebra' an instance again #19191 Closed

[Merged by Bors] - chore(field_theory.finite.galois_field, number_theory.cyclotomic.basic): make splitting_field.algebra' an instance again #19191

mathlib3
[Merged by Bors] - chore(field_theory.finite.galois_field, number_theory.cyclotomic.basic): make splitting_field.algebra' an instance again
#19191

Closed