Structures · Algebra
IsIntegralClosure
IsIntegralClosure A R B is the characteristic predicate stating A is
the integral closure of R in B,
i.e. that an element of B is integral over R iff it is an element of (the image of) A.
- Shape
- 3 explicit arguments · adds algebraMap_injective, isIntegral_iff
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances2
- NumberField.RingOfIntegers
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by161
- FractionalIdeal.dual
- IsIntegralClosure.algebraMap_injective
- IsIntegralClosure.isIntegral_iff
- IsIntegralClosure.isLocalization
- galRestrict
- IsIntegralClosure.mk'
- IsIntegralClosure.equiv
- galLift
- IsIntegralClosure.isIntegral_algebra
- IsIntegralClosure.algebraMap_mk'
- IsIntegralClosure.isIntegral
- coeIdeal_differentIdeal
- IsIntegralClosure.isFractionRing_of_finite_extension
- IsIntegralClosure.lift
- galRestrict'
- IsIntegralClosure.isDedekindDomain
- FractionalIdeal.coe_dual_one
- Rat.HeightOneSpectrum.primesEquiv
- Rat.IsIntegralClosure.intEquiv
- galRestrictHom
- Rat.HeightOneSpectrum.adicCompletion.padicEquiv
- FractionalIdeal.dual_ne_zero
- IsIntegralClosure.algebraMap_equiv
- Rat.HeightOneSpectrum.natGenerator
- Algebra.algebraMap_intTrace
- Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv
- FractionalIdeal.dual_zero
- IsIntegralClosure.MulSemiringAction
- galLiftEquiv
- galLift_algebraMap_apply
- FractionalIdeal.dual_eq_mul_inv
- Algebra.algebraMap_intNorm
- IsIntegralClosure.finite
- IsIntegralClosure.algebraMap_lift
- FractionalIdeal.dual.congr_simp
- algebraMap_galRestrict'_apply
- IsDedekindDomain.differentIdeal_eq_map_differentIdeal
- IsIntegralClosure.isNoetherian
- FractionalIdeal.coe_dual
- Module.Basis.ofIsCoprimeDifferentIdeal
- FractionalIdeal.mem_dual
- NumberField.not_dvd_discr_iff_forall_liesOver
- algebraMap_galRestrictHom_apply
- Algebra.map_intNormAux
- IsIntegralClosure.isTorsionFree
- Padic.adicCompletionEquiv
- PadicInt.adicCompletionIntegersEquiv
- Algebra.map_intTraceAux
- NumberField.RingOfIntegers.withValEquiv
- differentialIdeal_le_iff
Ancestors0
No ancestors.