mathlib3

f1637e56 - feat(field_theory/splitting_field): definition of splitting field (#3272)