[`FieldTheory/Perfect`] Prove equivalences

[SnirBroshi]

Prove all equivalent definitions from Wikipedia which don't already exist.

For example, perfectField_iff_splits_of_natSepDegree_eq_one already exists, but "the separable closure of k is algebraically closed" only has one side of the implication.

Also prove this nice MathOverflow theorem.