Documentation Verification Report

AlmostIntegral

📁 Source: Mathlib/RingTheory/IntegralClosure/IsIntegral/AlmostIntegral.lean

Statistics

Metric	Count
Definitions `IsAlmostIntegral`, `completeIntegralClosure`	2
Theorems `isIntegral`, `isIntegral_of_nonZeroDivisors_le_comap`, `isAlmostIntegral`, `isAlmostIntegral_of_exists_smul_mem_range`, `isAlmostIntegral_of_isLocalization`, `completeIntegralClosure_eq_integralClosure`, `integralClosure_le_completeIntegralClosure`, `isAlmostIntegral_iff_isIntegral`, `mem_completeIntegralClosure`	9
Total	11

IsAlmostIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isIntegral` 📖	mathematical	`IsAlmostIntegral`	`IsIntegral` `CommRing.toRing`	—	`IsDomain.of_faithfulSMul` `isIntegral_of_nonZeroDivisors_le_comap` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsDomain.to_noZeroDivisors` `IsDomain.toNontrivial`
`isIntegral_of_nonZeroDivisors_le_comap` 📖	mathematical	`IsAlmostIntegral` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Submonoid.comap` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `RingHom` `RingHom.instFunLike` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `algebraMap`	`IsIntegral` `CommRing.toRing`	—	`MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `IsScalarTower.right` `OreLocalization.instIsScalarTower` `Algebra.adjoin_eq_span` `Submonoid.powers_eq_closure` `Submodule.span_le` `Submodule.mem_span_singleton` `Localization.isLocalization` `map_pow` `Localization.mk_eq_mk'` `mul_assoc` `map_one` `MonoidHomClass.toOneHomClass` `mul_one` `Algebra.smul_def` `IsScalarTower.algebraMap_apply` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `mul_left_comm` `IsLocalization.injective` `Submonoid.powers_le` `Module.Finite.iff_fg` `Module.Finite.of_injective` `isNoetherian_of_isNoetherianRing_of_finite` `Module.Finite.span_singleton` `IsIntegral.of_mem_of_fg` `Algebra.self_mem_adjoin_singleton`

IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAlmostIntegral` 📖	mathematical	`IsIntegral` `CommRing.toRing`	`IsAlmostIntegral`	—	`isAlmostIntegral_of_isLocalization` `le_rfl`
`isAlmostIntegral_of_exists_smul_mem_range` 📖	mathematical	`IsIntegral` `CommRing.toRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors` `Subring` `Subring.instSetLike` `RingHom.range` `algebraMap` `Algebra.toSMul`	`IsAlmostIntegral`	—	`pow_mem` `Submonoid.instSubmonoidClass` `LT.lt.le` `pow_add` `SemigroupAction.mul_smul` `smul_pow` `IsScalarTower.right` `Algebra.to_smulCommClass` `Subalgebra.smul_mem` `Subalgebra.pow_mem` `Nat.strong_induction_on` `lt_or_ge` `minpoly.aeval` `one_smul` `minpoly.monic` `Polynomial.coeff_natDegree` `add_eq_zero_iff_eq_neg'` `Finset.sum_range_succ` `Polynomial.aeval_eq_sum_range` `mul_neg` `smul_neg` `Finset.mul_sum` `Finset.smul_sum` `Finset.sum_congr` `mul_smul_comm` `SMulCommClass.smul_comm` `smulCommClass_self` `NegMemClass.neg_mem` `SubringClass.toNegMemClass` `Subring.instSubringClass` `sum_mem` `SubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass`
`isAlmostIntegral_of_isLocalization` 📖	mathematical	`IsIntegral` `CommRing.toRing` `Submonoid` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submonoid.instPartialOrder` `nonZeroDivisors` `Semiring.toMonoidWithZero`	`IsAlmostIntegral`	—	`IsLocalization.exists_mk'_eq` `isAlmostIntegral_of_exists_smul_mem_range` `IsLocalization.smul_mk'_self`

(root)

Definitions

Name	Category	Theorems
`IsAlmostIntegral` 📖	MathDef	5 math math: `IsIntegral.isAlmostIntegral`, `IsIntegral.isAlmostIntegral_of_exists_smul_mem_range`, `isAlmostIntegral_iff_isIntegral`, `mem_completeIntegralClosure`, `IsIntegral.isAlmostIntegral_of_isLocalization`
`completeIntegralClosure` 📖	CompOp	3 math math: `integralClosure_le_completeIntegralClosure`, `completeIntegralClosure_eq_integralClosure`, `mem_completeIntegralClosure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`completeIntegralClosure_eq_integralClosure` 📖	mathematical	—	`completeIntegralClosure` `integralClosure`	—	`SetLike.ext` `isAlmostIntegral_iff_isIntegral`
`integralClosure_le_completeIntegralClosure` 📖	mathematical	—	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `integralClosure` `completeIntegralClosure`	—	`IsIntegral.isAlmostIntegral`
`isAlmostIntegral_iff_isIntegral` 📖	mathematical	—	`IsAlmostIntegral` `IsIntegral` `CommRing.toRing`	—	`IsAlmostIntegral.isIntegral` `IsFractionRing.isDomain` `IsFractionRing.instFaithfulSMul` `IsIntegral.isAlmostIntegral`
`mem_completeIntegralClosure` 📖	mathematical	—	`Subalgebra` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `SetLike.instMembership` `Subalgebra.instSetLike` `completeIntegralClosure` `IsAlmostIntegral`	—	—

---

← Back to Index