Theorems · Definition · field theory
AlgebraicClosure
(k : Type u) → [Field k] → Type u
The canonical algebraic closure of a field, the direct limit of adding roots to the field for each polynomial over the field.
- Cited by
- 53 results in Mathlib
- Foundations
- Depth 161 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement and proof · cited by 7,404
- HasQuotient.Quotientproof · cited by 2,301
- MvPolynomialproof · cited by 2,140
- AlgebraicClosure.Varsproof · cited by 4
- AlgebraicClosure.maxIdealproof · cited by 2
Cited by67
Results whose statement or proof uses this declaration.
- PadicAlgClproof · cited by 21
- IsCyclotomicExtension.isGaloisproof · cited by 13
- Field.Embproof · cited by 12
- Algebra.isIntegral_traceproof · cited by 7
- Algebra.FormallyUnramified.isReduced_of_fieldproof · cited by 6
- spectralNorm.eq_of_normalClosurestatement · cited by 5
- Algebra.norm_eq_prod_automorphismsproof · cited by 5
- Algebra.isIntegral_normproof · cited by 4
- Polynomial.natSepDegree_expandproof · cited by 4
- Polynomial.natSepDegree_powproof · cited by 4
- IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomicproof · cited by 3
- isPowMul_spectralNormproof · cited by 3