mathlib

d57ac08c - feat(field_theory/separable): definition and basic properties (#3155)