mathlib

2ed7c0ff - doc(field_theory/galois): add comment that separable extensions are a… (#10500)

doc(field_theory/galois): add comment that separable extensions are a… (#10500) …lgebraic I teach my students that a Galois extension is algebraic, normal and separable, and was just taken aback when I read the mathlib definition which omits "algebraic". Apparently there are two conventions for the definition of separability, one implying algebraic and the other not: https://en.wikipedia.org/wiki/Separable_extension#Separability_of_transcendental_extensions . Right now we have separability implies algebraic in mathlib so mathematically we're fine; I just add a note to clarify what's going on. In particular if we act on the TODO in the separability definition, we may (perhaps unwittingly) break the definition of `is_galois`; hopefully this note lessens the chance that this happens.