Commit 2024-11-16 00:52 118a685f

feat(FieldTheory/SeparableDegree): Field.Emb is infinite for transcendental extension (#18770)

• Field.infinite_emb_of_transcendental, Field.finSepDegree_eq_zero_of_transcendental: Field.Emb is infinite and Field.finSepDegree is zero for transcendental extensions
• remove algebraic assumptions in isPurelyInseparable_(of|iff)_finSepDegree_eq_one
• prove IsPurelyInseparable.of_injective_comp_algebraMap
• change Field.Emb from def to abbrev