Documentation Verification Report

Completeness

📁 Source: Mathlib/RingTheory/AdicCompletion/Completeness.lean

Statistics

Metric	Count
Definitions `ofPowSMul`, `ofValEqZero`, `ofValEqZeroAux`	3
Theorems `isAdicComplete`, `ofPowSMul_injective`, `ofPowSMul_ofValEqZero`, `ofPowSMul_val_apply`, `ofPowSMul_val_apply_eq_zero`, `pow_smul_top_eq_ker_eval`, `restrictScalars_range_ofPowSMul_eq_ker_eval`	7
Total	10

AdicCompletion

Definitions

Name	Category	Theorems
`ofPowSMul` 📖	CompOp	5 math math: `ofPowSMul_ofValEqZero`, `ofPowSMul_injective`, `ofPowSMul_val_apply_eq_zero`, `restrictScalars_range_ofPowSMul_eq_ker_eval`, `ofPowSMul_val_apply`
`ofValEqZero` 📖	CompOp	1 math math: `ofPowSMul_ofValEqZero`
`ofValEqZeroAux` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAdicComplete` 📖	mathematical	`Ideal.FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`IsAdicComplete` `AdicCompletion` `instAddCommGroup` `instModuleOfIsScalarTower` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `AddCommGroup.toAddCommMonoid` `Module.toDistribMulAction`	—	`IsScalarTower.left` `instIsHausdorff` `IsScalarTower.right` `transitionMap_comp_eval_apply` `eval_apply` `sub_eq_zero` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `LinearMap.mem_ker` `instIsScalarTower` `pow_smul_top_eq_ker_eval` `SModEq.sub_mem` `sub_self`
`ofPowSMul_injective` 📖	mathematical	—	`AdicCompletion` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `Top.top` `Submodule.instTop` `Submodule.addCommGroup` `CommRing.toRing` `Submodule.module` `DFunLike.coe` `LinearMap` `LieRing.toAddCommGroup` `LieRing.ofAssociativeRing` `LieAlgebra.toModule` `LieAlgebra.ofAssociativeAlgebra` `instCommRing` `RingHom.id` `Semiring.toNonAssocSemiring` `instAddCommGroup` `module` `LinearMap.instFunLike` `ofPowSMul`	—	`IsScalarTower.left` `IsScalarTower.right` `LinearMap.ker_eq_bot` `LinearMap.ker_eq_bot'` `ext` `Submodule.isScalarTower'` `add_comm` `LinearMap.map_eq_zero_iff` `Submodule.powSMulQuotInclusion_injective` `ofPowSMul_val_apply`
`ofPowSMul_ofValEqZero` 📖	mathematical	`HasQuotient.Quotient` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `CommRing.toRing` `Ideal` `Submodule.instSMul` `Semiring.toModule` `Submodule.instPowNat` `Top.top` `Submodule.instTop` `Submodule.Quotient.instZeroQuotient`	`DFunLike.coe` `LinearMap` `AdicCompletion` `LieRing.toAddCommGroup` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.toModule` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `instCommRing` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.instPowNat` `IsScalarTower.right` `Top.top` `Submodule.instTop` `Submodule.addCommGroup` `Submodule.module` `instAddCommGroup` `module` `LinearMap.instFunLike` `ofPowSMul` `ofValEqZero`	—	`ext` `IsScalarTower.left` `IsScalarTower.right` `Submodule.isScalarTower'` `ofPowSMul_val_apply` `ofPowSMul_val_apply_eq_zero` `LT.lt.le` `Subtype.prop` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`ofPowSMul_val_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `AdicCompletion` `LieRing.toAddCommGroup` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.toModule` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `instCommRing` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.instPowNat` `IsScalarTower.right` `Top.top` `Submodule.instTop` `Submodule.addCommGroup` `Submodule.module` `instAddCommGroup` `module` `LinearMap.instFunLike` `ofPowSMul` `HasQuotient.Quotient` `Submodule.addCommMonoid` `Submodule.hasQuotient` `Submodule.isScalarTower'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `DistribSMul.toSMulZeroClass` `instDistribSMul` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `DistribMulAction.toDistribSMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `Submodule.powSMulQuotInclusion`	—	`IsScalarTower.left` `IsScalarTower.right` `Submodule.isScalarTower'` `Subtype.prop` `Ideal.instIsTwoSided_1` `map_val_apply` `Submodule.Quotient.induction_on`
`ofPowSMul_val_apply_eq_zero` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `AdicCompletion` `LieRing.toAddCommGroup` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.toModule` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `instCommRing` `RingHom.id` `Semiring.toNonAssocSemiring` `Submodule` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Ideal` `Submodule.instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.instPowNat` `IsScalarTower.right` `Top.top` `Submodule.instTop` `Submodule.addCommGroup` `Submodule.module` `instAddCommGroup` `module` `LinearMap.instFunLike` `ofPowSMul` `HasQuotient.Quotient` `Submodule.hasQuotient` `Submodule.Quotient.instZeroQuotient`	—	`IsScalarTower.left` `IsScalarTower.right` `Ideal.instIsTwoSided_1` `map_val_apply` `Submodule.Quotient.induction_on` `Submodule.pow_smul_top_le` `Subtype.prop`
`pow_smul_top_eq_ker_eval` 📖	mathematical	`Ideal.FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule` `AdicCompletion` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `instModuleOfIsScalarTower` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Submodule.instSMul` `Semiring.toModule` `instIsScalarTower` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Submodule.instPowNat` `IsScalarTower.right` `Top.top` `Submodule.instTop` `LinearMap.ker` `HasQuotient.Quotient` `Submodule.hasQuotient` `CommRing.toRing` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `RingHom.id` `eval`	—	`le_antisymm` `IsScalarTower.left` `instIsScalarTower` `IsScalarTower.right` `pow_smul_top_le_ker_eval` `Ideal.FG.pow` `Ideal.instIsTwoSided_1` `Submodule.span_smul_eq` `instIsScalarTower_1` `Submodule.restrictScalars_top` `Submodule.restrictScalars_image_smul_eq` `RingHomSurjective.ids` `restrictScalars_range_ofPowSMul_eq_ker_eval` `Submodule.restrictScalars_le` `RingHomInvPair.ids` `smulCommClass_self` `Submodule.image_smul_top_eq_range_lsum` `RingHomCompTriple.ids` `LinearMap.range_comp_of_range_eq_top` `LinearEquiv.range` `RingHomSurjective.invPair` `LinearMap.range_eq_top_of_surjective` `map_comp` `LinearEquiv.self_trans_symm` `map_id` `Submodule.smul_top_eq_range_lsum` `LinearMap.range_eq_top` `LinearMap.range_codRestrict` `Submodule.comap_subtype_self` `map_surjective` `LinearMap.comp_apply` `RingHomCompTriple.right_ids` `LinearMap.subtype_comp_codRestrict`
`restrictScalars_range_ofPowSMul_eq_ker_eval` 📖	mathematical	—	`Submodule.restrictScalars` `AdicCompletion` `LieRing.toAddCommGroup` `LieRing.ofAssociativeRing` `CommRing.toRing` `LieAlgebra.toModule` `LieAlgebra.ofAssociativeAlgebra` `Algebra.id` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `instCommRing` `AddCommGroup.toAddCommMonoid` `instAddCommGroup` `instModuleOfIsScalarTower` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `module` `instSMul` `IsScalarTower.right` `instIsScalarTower_1` `LinearMap.range` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Ideal` `Submodule.instSMul` `Semiring.toModule` `Submodule.instPowNat` `Top.top` `Submodule.instTop` `Submodule.addCommGroup` `Submodule.module` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `ofPowSMul` `LinearMap.ker` `HasQuotient.Quotient` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module` `eval`	—	`le_antisymm` `IsScalarTower.left` `IsScalarTower.right` `instIsScalarTower_1` `RingHomSurjective.ids` `LinearMap.mem_ker` `eval_apply` `ofPowSMul_val_apply_eq_zero` `le_refl` `ofPowSMul_ofValEqZero`

---

← Back to Index