Commit 2023-11-01 13:33 3ef1fe9c

refactor: golf Normal.of_isSplittingField (#8004) Before: Construction only imports Normal, which transitively imports IsSplittingField Now: Normal imports Construction, Construction only imports IsSplittingField So no extra transitive import is added to any file other than Construction and Normal. As a consequence, Polynomial.SplittingField.instNormal is moved from Construction to Normal. adjoin_rootSet_eq_range is added to IsSplittingField. splits_of_comp in Splits is extracted from splits_of_splits in IsSplittingField. Source of proof: https://math.stackexchange.com/a/2585087/12932 Move Algebra.adjoin.liftSingleton from IsAlgClosed/Basic to Adjoin/Field in order to speed up lift_of_splits (renamed to add namespace Polynomial).