Structures · Algebra
Algebra.IsIntegral
An algebra is integral if every element of the extension is integral over the base ring.
- Shape
- 2 explicit arguments · adds isIntegral
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances6
- Int
- Polynomial
- NumberField.RingOfIntegers
- MvPolynomial
- Localization.AtPrime
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by210
- Algebra.IsIntegral.isIntegral
- Algebra.intNorm
- Algebra.normalizedTrace
- isIntegral_trans
- NumberField.IsCMField.complexConj
- Ideal.eq_bot_of_comap_eq_bot
- IsIntegralClosure.lift
- isAlgebraic_of_isFractionRing
- Algebra.algebraMap_intNorm_fractionRing
- IsAlgClosed.algebraMap_bijective_of_isIntegral
- Ideal.isMaximal_of_isIntegral_of_isMaximal_comap
- Ideal.exists_ideal_over_maximal_of_isIntegral
- Ideal.eq_bot_of_liesOver_bot
- NumberField.IsCMField.unitsComplexConj
- IsGaloisGroup.of_isFractionRing
- Algebra.IsIntegral.finite
- IsPrimitiveRoot.intermediateField_adjoin_isCyclotomicExtension
- IsDedekindDomain.primesOver_ncard_ne_zero
- Ideal.IsMaximal.of_liesOver_isMaximal
- Ideal.IsIntegral.comap_ne_bot
- Ideal.ramificationIdx_eq_one_iff
- isField_of_isIntegral_of_isField
- Algebra.algebraMap_intNorm
- isIntegral_localization
- IsAlgebraic.restrictScalars_of_isIntegral
- IsIntegralClosure.algebraMap_lift
- Algebra.normalizedTrace_algebraMap_apply
- Ideal.exists_maximal_ideal_liesOver_of_isIntegral
- Ideal.IsIntegral.comap_lt_comap
- NumberField.CMExtension.equivMaximalRealSubfield
- FractionalIdeal.coe_extendedHom_eq_span
- isField_of_isIntegral_of_isField'
- Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton
- Ideal.isMaximal_comap_of_isIntegral_of_isMaximal
- Algebra.IsIntegral.tower_top
- Ideal.IsIntegral.isMaximal_of_isMaximal_comap
- FractionalIdeal.extendedHom_le_one_iff
- NumberField.IsCMField.ringOfIntegersComplexConj
- Ideal.exists_ideal_over_prime_of_isIntegral
- Algebra.intNorm_eq_norm
- Subalgebra.LinearDisjoint.of_linearDisjoint_finite_left
- FractionalIdeal.le_one_of_extendedHom_le_one
- NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff
- Transcendental.extendScalars_of_isIntegral
- NumberField.IsCMField.complexEmbedding_complexConj
- Algebra.normalizedTrace_map
- Algebra.intNorm_zero
- IsFractionRing.isInvariant_of_isIntegral
- Ideal.IsMaximal.ne_bot_of_isIntegral_int
- IsGaloisGroup.to_isFractionRing_of_isIntegral
Ancestors0
No ancestors.