mathlib

517f0b5c - feat(ring_theory/polynomial/basic): prerequisites for galois_definition (#4829)