Documentation Verification Report

Defs

📁 Source: Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Defs.lean

Statistics

MetricCount
DefinitionsIsIntegralClosure
1
TheoremsalgebraMap_injective, isIntegral_iff
2
Total3

IsIntegralClosure

Theorems

NameKindAssumesProvesValidatesDepends On
algebraMap_injective 📖mathematical—DFunLike.coe
RingHom
Semiring.toNonAssocSemiring
CommSemiring.toSemiring
CommRing.toCommSemiring
RingHom.instFunLike
algebraMap		——
isIntegral_iff 📖mathematical—IsIntegral
CommRing.toRing
DFunLike.coe
RingHom
Semiring.toNonAssocSemiring
CommSemiring.toSemiring
CommRing.toCommSemiring
RingHom.instFunLike
algebraMap		——

(root)

Definitions

NameCategoryTheorems
IsIntegralClosure 📖CompData
21 mathmath: IsIntegralClosure.of_isIntegrallyClosedIn, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow, NumberField.RingOfIntegers.instIsIntegralClosureIntWithVal, IsDedekindRing.toIsIntegralClosure, IsIntegralClosure.of_isIntegrallyClosed, FunctionField.ringOfIntegers.instIsIntegralClosureSubtypeMemSubalgebraPolynomial, IsIntegralClosure.of_algEquiv, IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime, algebraicClosure.isIntegralClosure, IsIntegralClosure.tower_top, IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure, IsIntegralClosure.of_isIntegralClosure_of_isIntegrallyClosedIn, NumberField.RingOfIntegers.instIsIntegralClosureInt, IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime, IsIntegrallyClosed.instIsIntegralClosure, integralClosure.isIntegralClosure, isIntegrallyClosed_iff_isIntegralClosure, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton, Ring.instIsIntegralClosureNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure, NumberField.RingOfIntegers.instIsIntegralClosure

---

← Back to Index