Structures · Algebra
IsAlgClosed
An algebraically closed field is one where every polynomial splits. Equivalently, all
non-constant polynomials have a root. See IsAlgClosed.exists_root and
IsAlgClosed.of_exists_root.
- Defined in
- Mathlib.FieldTheory.IsAlgClosed.Basic
- Shape
- One type argument · adds splits
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- Complex
- PadicComplex
- AlgebraicClosure
How is a type an instance?
Loading the hierarchy index…
Assumed by163
- IsAlgClosed.splits
- AlgHom.card
- Polynomial.natSepDegree_eq_of_isAlgClosed
- IsAlgClosed.exists_root
- AlgebraicGeometry.residueFieldIsoBase
- AlgebraicGeometry.pointOfClosedPoint
- NumberField.Embeddings.card
- IsAlgClosed.algebraMap_bijective_of_isIntegral
- WittVector.RecursionBase.solution
- WittVector.RecursionMain.succNthVal
- Algebra.norm_eq_prod_embeddings
- IsAlgClosed.lift
- WittVector.frobeniusRotation
- AlgebraicGeometry.pointEquivClosedPoint
- NumberField.Embeddings.finite_of_norm_le
- IsAlgClosed.exists_aeval_eq_zero
- Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two
- IsAlgClosed.card_roots_eq_natDegree
- WittVector.frobeniusRotationCoeff
- NumberField.Embeddings.coeff_bdd_of_norm_le
- trace_eq_sum_embeddings
- AlgebraicGeometry.pointOfClosedPoint_comp
- IsAlgClosed.exists_pow_nat_eq
- spectrum.nonempty_of_isAlgClosed_of_finiteDimensional
- AlgebraicGeometry.SpecMap_residueFieldIsoBase_inv
- MvPolynomial.eq_vanishingIdeal_singleton_of_isMaximal
- IsAlgClosed.roots_eq_zero_iff_natDegree_eq_zero
- IsAlgClosed.exists_eval₂_eq_zero_of_injective
- CategoryTheory.finrank_hom_simple_simple_le_one
- Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans
- IsAlgClosed.degree_eq_one_of_irreducible
- spectrum.map_polynomial_aeval_of_nonempty
- IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed
- CategoryTheory.finrank_hom_simple_simple_eq_one_iff
- NumberField.Embeddings.pow_eq_one_of_norm_le_one
- IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_lt
- AlgebraicGeometry.ext_of_apply_closedPoint_eq
- QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed
- IsAlgClosed.dvd_iff_roots_le_roots
- spectrum.map_polynomial_aeval_of_degree_pos
- WittVector.RecursionBase.solution_spec
- CategoryTheory.finrank_endomorphism_simple_eq_one
- IsAlgClosed.cardinal_le_max_transcendence_basis
- QuadraticForm.isometryEquivSumSquaresUnits
- Algebra.discr_powerBasis_eq_prod'
- IsAlgClosed.ringEquiv_of_equiv_of_char_eq
- FDRep.char_orthonormal
- Algebra.discr_powerBasis_eq_prod''
- Module.End.exists_eigenvalue
- Representation.IsIrreducible.finrank_intertwiningMap_self
Ancestors0
No ancestors.