Documentation Verification Report

Pure

📁 Source: Mathlib/RingTheory/Ideal/Pure.lean

Statistics

Metric	Count
Definitions `Pure`	1
Theorems `of_inf_eq_mul`, `of_isIdempotentElem`, `exists_eq_mul_of_pure`, `inf_eq_mul_of_pure`, `isIdempotentElem_of_pure`, `ker_piRingHom_atPrime_eq_of_pure`, `le_ker_atPrime_of_forall_exists_eq_mul`, `zeroLocus_inj_of_pure`, `injective_lTensor_quotient_iff_inf_eq_mul`	9
Total	10

Ideal

Definitions

Name	Category	Theorems
`Pure` 📖	MathDef	2 math math: `Pure.of_inf_eq_mul`, `Pure.of_isIdempotentElem`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_eq_mul_of_pure` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`IsScalarTower.right` `inf_eq_mul_of_pure` `subset_span` `IsScalarTower.left` `mem_mul_span_singleton` `instIsTwoSided_1`
`inf_eq_mul_of_pure` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.mul` `IsScalarTower.right` `Algebra.id`	—	`IsScalarTower.right` `injective_lTensor_quotient_iff_inf_eq_mul` `Module.Flat.lTensor_preserves_injective_linearMap` `Submodule.injective_subtype`
`isIdempotentElem_of_pure` 📖	mathematical	—	`IsIdempotentElem` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id`	—	`IsScalarTower.right` `inf_of_le_left` `instReflLe`
`ker_piRingHom_atPrime_eq_of_pure` 📖	mathematical	—	`RingHom.ker` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Pi.nonAssocSemiring` `Set.Elem` `PrimeSpectrum` `PrimeSpectrum.zeroLocus` `SetLike.coe` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Localization.AtPrime` `PrimeSpectrum.asIdeal` `Set` `Set.instMembership` `PrimeSpectrum.isPrime` `OreLocalization.instSemiring` `primeCompl` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `Pi.semiring` `RingHom.instFunLike` `RingHom.instRingHomClass` `Pi.ringHom` `algebraMap` `CommSemiring.toCommMonoid` `OreLocalization.instAlgebra` `Algebra.id`	—	`le_antisymm` `PrimeSpectrum.isPrime` `RingHom.instRingHomClass` `Pi.ker_ringHom` `le_trans` `iInf_le_of_le` `le_rfl` `iInf_ker_le` `RingHom.mem_ker` `Pi.ringHom_apply` `Pi.zero_apply` `le_ker_atPrime_of_forall_exists_eq_mul` `exists_eq_mul_of_pure`
`le_ker_atPrime_of_forall_exists_eq_mul` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `RingHom.ker` `Localization.AtPrime` `RingHom` `OreLocalization.instSemiring` `primeCompl` `OreLocalization.oreSetComm` `CommSemiring.toCommMonoid` `RingHom.instFunLike` `RingHom.instRingHomClass` `algebraMap` `OreLocalization.instAlgebra` `Algebra.id`	—	`RingHom.instRingHomClass` `IsLocalization.algebraMap_isUnit_iff` `Localization.isLocalization` `one_notMem` `sub_add_cancel` `add_mem` `mul_sub` `mul_one` `sub_self` `IsUnit.mul_left_eq_zero` `RingHom.map_zero`
`zeroLocus_inj_of_pure` 📖	mathematical	—	`PrimeSpectrum.zeroLocus` `CommRing.toCommSemiring` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`PrimeSpectrum.isPrime` `RingHom.instRingHomClass` `ker_piRingHom_atPrime_eq_of_pure`

Ideal.Pure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_inf_eq_mul` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instMin` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submodule.mul` `IsScalarTower.right` `Algebra.id`	`Ideal.Pure`	—	`IsScalarTower.right` `eq_1` `Module.Flat.iff_lTensor_injective` `injective_lTensor_quotient_iff_inf_eq_mul`
`of_isIdempotentElem` 📖	mathematical	`Ideal.FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `IsIdempotentElem` `Ideal` `Submodule.mul` `Semiring.toModule` `IsScalarTower.right` `Algebra.id`	`Ideal.Pure`	—	`IsScalarTower.right` `Ideal.isIdempotentElem_iff_of_fg` `Module.Flat.of_linearEquiv` `Module.Flat.of_free` `Module.Free.self` `RingHomInvPair.ids` `IsIdempotentElem.one_sub` `add_sub_cancel` `Module.Flat.of_retract`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`injective_lTensor_quotient_iff_inf_eq_mul` 📖	mathematical	—	`TensorProduct` `CommRing.toCommSemiring` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `Ideal.instHasQuotient_1` `Submodule` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Ideal.Quotient.commRing` `Submodule.addCommMonoid` `Submodule.Quotient.module` `CommRing.toRing` `Ring.toAddCommGroup` `Submodule.module` `DFunLike.coe` `LinearMap` `RingHom.id` `TensorProduct.addCommMonoid` `TensorProduct.instModule` `LinearMap.instFunLike` `LinearMap.lTensor` `Submodule.subtype` `Submodule.instMin` `Submodule.mul` `IsScalarTower.right` `Algebra.id`	—	`Submodule.isScalarTower'` `IsScalarTower.right` `RingHomSurjective.ids` `IsScalarTower.left` `Submodule.map_smul''` `Submodule.map_top` `Submodule.range_subtype` `Ideal.instIsTwoSided_1` `RingHomCompTriple.ids` `RingHomInvPair.ids` `TensorProduct.AlgebraTensorModule.curry_injective` `Ideal.Quotient.isScalarTower` `TensorProduct.isScalarTower` `Submodule.linearMap_qext` `IsScalarTower.to_smulCommClass` `LinearMap.ext_ring` `LinearMap.ext` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `TensorProduct.quotTensorEquivQuotSMul_mk_one_tmul` `Algebra.TensorProduct.tmul_one_eq_one_tmul` `EquivLike.toEmbeddingLike` `Submodule.ker_mapQ` `Submodule.ker_mkQ` `Submodule.map_le_map_iff_of_injective` `Submodule.injective_subtype` `Submodule.map_comap_subtype` `inf_comm` `Ideal.mul_le_inf`

---

← Back to Index