Commit 2024-07-04 13:06 085aa587

View on Github →

feat(FieldTheory/Separable): add elementwise IsSeparable and rename the old to Algebra.IsSeparable (#14232) Make IsSeparable more aligned with IsIntegral. Rename previous IsSeparable into Algebra.IsSeparable (like Algebra.IsIntegral), add notation IsSeparable for separablity of elements (like IsIntegral). Shorten statements using the new defined IsSeparable. Rename some shortened theorems.

Estimated changes

modified theorem IsGalois.separable
modified theorem isGalois_iff
modified theorem AlgEquiv.isSeparable
modified theorem AlgEquiv.isSeparable_iff
modified theorem AlgHom.card_of_powerBasis
modified theorem IsSeparable.isIntegral
deleted theorem IsSeparable.of_algHom
deleted theorem IsSeparable.separable
added def IsSeparable
deleted theorem isSeparable_iff
deleted theorem IsSeparable.sepDegree_eq
modified theorem le_separableClosure'
modified theorem le_separableClosure
modified theorem separableClosure.eq_top_iff
added theorem Field.isSeparable_add
added theorem Field.isSeparable_inv
added theorem Field.isSeparable_mul
deleted theorem Field.separable_add
deleted theorem Field.separable_inv
deleted theorem Field.separable_mul
deleted theorem IsSeparable.trans
modified theorem RingOfIntegers.coe_norm
modified theorem RingOfIntegers.norm_norm
modified def Algebra.intNormAux
modified theorem Algebra.map_intNormAux
modified theorem Algebra.isIntegral_norm
modified theorem Algebra.norm_eq_norm_adjoin
modified theorem Algebra.norm_eq_prod_roots
modified theorem Algebra.norm_norm
modified theorem Algebra.trace_ne_zero
modified theorem Algebra.trace_surjective
modified theorem det_traceForm_ne_zero
modified theorem det_traceMatrix_ne_zero'
modified theorem traceForm_nondegenerate
modified theorem trace_eq_sum_embeddings