AlgebraicClosure 📖 | CompOp | 36 mathmath: Field.Emb.Cardinal.equivLim_coherence, IntermediateField.instIsAlgClosureAlgebraicClosureSubtypeMemOfIsAlgebraic, SeparableClosure.isSepClosed, Field.Emb.Cardinal.instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, IntermediateField.AdjoinDouble.normal_algebraicClosure, Algebra.isGeometricallyReduced_iff, Field.Emb.Cardinal.succEquiv_coherence, Ring.instIsScalarTowerSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, AlgebraicClosure.hasEnoughRootsOfUnity, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure_1, Field.absoluteGaloisGroup.commutator_closure_isNormal, Algebra.IsGeometricallyReduced.isReduced_algebraicClosure_tensorProduct, AlgebraicClosure.instIsAlgClosureOfIsAlgebraic, AlgebraicClosure.instCharP, SeparableClosure.hasEnoughRootsOfUnity_pow, Ring.instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, Field.Emb.Cardinal.equivSucc_coherence, instSeminormClassAlgebraNormSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, SeparableClosure.hasEnoughRootsOfUnity, AlgebraicClosure.instIsAlgClosure, Ring.instIsSeparableFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, Ring.instIsScalarTowerFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, AlgebraicClosure.Monics.map_eq_prod, spectralNorm.eq_of_normalClosure, Ring.instFiniteDimensionalFractionRingSubtypeAlgebraicClosureMemIntermediateFieldNormalClosure, spectralNorm.eq_of_normalClosure', IntermediateField.AdjoinSimple.normal_algebraicClosure, AlgebraicClosure.instIsScalarTower, Ring.instFaithfulSMulSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, AlgebraicClosure.isAlgebraic, AlgebraicClosure.isAlgClosed, Ring.instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, Ring.instIsScalarTowerNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure_1, AlgebraicClosure.instCharZero, AlgebraicClosure.hasEnoughRootsOfUnity_pow
|