Commit 2023-08-14 12:56 628cf18b

View on Github →

feat(Mathlib/FieldTheory/IsSepClosed) separably closed field and separable closure - basic definition (#6285) Main changes

Add IsSepClosed and basic properties.
Add IsSepClosure and basic properties.

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/IsSepClosed.lean

added theorem IsSepClosed.algebraMap_surjective

added theorem IsSepClosed.degree_eq_one_of_irreducible

added theorem IsSepClosed.exists_aeval_eq_zero

added theorem IsSepClosed.exists_eq_mul_self

added theorem IsSepClosed.exists_eval₂_eq_zero

added theorem IsSepClosed.exists_pow_nat_eq

added theorem IsSepClosed.exists_root

added theorem IsSepClosed.of_exists_root

added theorem IsSepClosed.roots_eq_zero_iff

added theorem IsSepClosed.splits_codomain

added theorem IsSepClosed.splits_domain

added theorem isSepClosure_iff