Documentation Verification Report

Index

📁 Source: Mathlib/RingTheory/Ideal/Quotient/Index.lean

Statistics

Metric	Count
Definitions `Index`, `Index`, `Index`, `Index`, `Index`	5
Theorems `finite_quotient_pow`, `finite_quotient_prod`, `index_pow_le`, `finite_quotient_smul`, `index_smul_le`	5
Total	10

CategoryTheory.Precoverage.ZeroHypercover.Small

Definitions

Name	Category	Theorems
`Index` 📖	CompOp	2 math math: `CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall_toPreZeroHypercover`, `mem₀`

CategoryTheory.Subfunctor.IsFinite

Definitions

Name	Category	Theorems
`Index` 📖	CompOp	4 math math: `CategoryTheory.Subfunctor.Subpresheaf.isGeneratedBy_of_isFinite`, `CategoryTheory.Subfunctor.isGeneratedBy_of_isFinite`, `instFiniteIndex`, `CategoryTheory.presheafIsGeneratedBy_of_isFinite`

CategoryTheory.Subfunctor.Subpresheaf.IsFinite

Definitions

Name	Category	Theorems
`Index` 📖	CompOp	—

FiberBundleCore

Definitions

Name	Category	Theorems
`Index` 📖	CompOp	—

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_quotient_pow` 📖	mathematical	`FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Finite` `HasQuotient.Quotient` `Ideal` `instHasQuotient_1` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IdemSemiring.toSemiring` `Submodule.idemSemiring` `Algebra.id`	—	`pow_zero` `one_eq_top` `Finite.of_fintype` `Submodule.finite_quotient_smul` `IsScalarTower.right`
`finite_quotient_prod` 📖	mathematical	`FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Finite` `HasQuotient.Quotient` `Ideal` `instHasQuotient_1`	`Finset.prod` `CommSemiring.toCommMonoid` `IdemCommSemiring.toCommSemiring` `instIdemCommSemiring`	—	`Finset.induction_on` `one_eq_top` `Finite.of_fintype` `Finset.prod_insert` `mul_comm` `Submodule.finite_quotient_smul`
`index_pow_le` 📖	mathematical	`span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.coe` `Finset` `Finset.instSetLike`	`AddSubgroup.index` `AddCommGroup.toAddGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Submodule.toAddSubgroup` `Semiring.toModule` `Ideal` `Submodule.instPowNat` `IsScalarTower.right` `Algebra.id` `Monoid.toNatPow` `Nat.instMonoid` `Finset.sum` `Nat.instAddCommMonoid` `Finset.range` `Finset.card`	—	`finite_quotient_pow` `IsScalarTower.right` `pow_zero` `one_eq_top` `AddSubgroup.index_top` `LE.le.trans` `IsScalarTower.left` `Submodule.index_smul_le` `le_rfl` `pow_mul` `pow_succ` `geom_sum_succ` `mul_comm` `le_refl`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_quotient_smul` 📖	mathematical	`FG` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	`Finite` `HasQuotient.Quotient` `Submodule` `hasQuotient` `CommRing.toRing` `Ideal` `instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`IsScalarTower.left` `RingHomInvPair.ids` `isScalarTower'` `RingHomCompTriple.ids` `map_injective_of_injective` `RingHomSurjective.ids` `injective_subtype` `map_comap_subtype` `inf_of_le_right` `map_smul''` `map_top` `range_subtype` `Nat.card_congr` `Module.Finite.of_fg` `Module.finite_of_finite` `Algebra.to_smulCommClass` `Module.Finite.base_change` `LT.lt.ne'` `Nat.card_pos` `AddSubgroup.relIndex_mul_index` `smul_le_right` `mul_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `AddSubgroup.index_ne_zero_of_finite` `AddSubgroup.finite_quotient_of_finiteIndex`
`index_smul_le` 📖	mathematical	`span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.coe` `Finset` `Finset.instSetLike`	`AddSubgroup.index` `AddCommGroup.toAddGroup` `toAddSubgroup` `CommRing.toRing` `Ideal` `Submodule` `instSMul` `Semiring.toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Monoid.toNatPow` `Nat.instMonoid` `Ring.toAddCommGroup` `Finset.card`	—	`nonempty_fintype` `IsScalarTower.left` `AddSubgroup.relIndex_mul_index` `smul_le_right` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `Nat.instMulLeftMono` `RingHomInvPair.ids` `isScalarTower'` `RingHomCompTriple.ids` `map_injective_of_injective` `RingHomSurjective.ids` `injective_subtype` `map_comap_subtype` `inf_of_le_right` `map_smul''` `map_top` `range_subtype` `Nat.card_congr` `Finsupp.range_linearCombination` `Subtype.range_val` `LinearMap.mem_range` `Eq.ge` `IsScalarTower.to_smulCommClass` `Ideal.Quotient.isScalarTower` `IsScalarTower.right` `LinearMap.lTensor_surjective` `LinearEquiv.surjective` `LE.le.trans` `Nat.card_le_card_of_surjective` `Finite.of_fintype` `Nat.card_eq_fintype_card` `Fintype.card_finsupp` `Fintype.card_coe`

VectorBundleCore

Definitions

Name	Category	Theorems
`Index` 📖	CompOp	—

---

← Back to Index