Structures · Algebra
Algebra.IsAlgebraic
An algebra is algebraic if all its elements are algebraic.
- Defined in
- Mathlib.RingTheory.Algebraic.Defs
- Shape
- 2 explicit arguments · adds isAlgebraic
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances7
- Polynomial
- Padic
- FractionRing
- MvPolynomial
- Ideal.ResidueField
- Subtype
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by306
- Algebra.IsAlgebraic.isAlgebraic
- IsIntegralClosure.isLocalization
- Field.Emb.Cardinal.leastExt
- galRestrict
- Algebra.IsAlgebraic.trans
- FiniteField.frobeniusAlgEquivOfAlgebraic
- galLift
- spectralAlgNorm
- NumberField.InfinitePlace.comap_surjective
- Field.Emb.Cardinal.filtration
- AlgEquiv.isAlgebraic
- IntermediateField.sup_toSubalgebra_of_isAlgebraic_right
- IsAlgebraic.restrictScalars
- Field.finSepDegree_mul_finSepDegree_of_isAlgebraic
- galRestrictHom
- Algebra.IsAlgebraic.nontrivial
- spectralMulAlgNorm
- NumberField.ComplexEmbedding.lift
- IsAlgClosed.lift
- Algebra.IsAlgebraic.algEquivEquivAlgHom
- Transcendental.extendScalars
- Algebra.IsAlgebraic.extendScalars
- Algebra.IsAlgebraic.algHom_bijective₂
- Field.Emb.Cardinal.isLeast_leastExt
- IsIntegralClosure.MulSemiringAction
- galLiftEquiv
- AlgebraicIndependent.extendScalars
- galLift_algebraMap_apply
- Algebra.IsAlgebraic.cardinalMk_le_max
- IntermediateField.exists_lt_finrank_of_infinite_dimensional
- NumberField.ComplexEmbedding.lift_comp_algebraMap
- Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits
- isPowMul_spectralNorm
- Field.nonempty_algHom_of_exists_root
- Field.Emb.Cardinal.embFunctor
- spectralNorm_unique
- Algebra.IsAlgebraic.algHom_bijective
- Algebra.IsAlgebraic.tower_top
- Algebra.IsAlgebraic.of_ringHom_of_comp_eq
- IntermediateField.algHomEquivAlgHomOfSplits
- Algebra.IsAlgebraic.ringHom_of_comp_eq
- Field.Emb.Cardinal.strictMono_leastExt
- Algebra.IsAlgebraic.isDomain_of_adjoin_range
- Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic
- AlgebraicIndependent.isEmpty_of_isAlgebraic
- exists_isTranscendenceBasis_subset
- JacobsonNoether.exists_pow_mem_center_of_inseparable
- Algebra.IsAlgebraic.perfectField
- Field.finSepDegree_eq
- algebraMap_galRestrictHom_apply
Ancestors0
No ancestors.