Documentation Verification Report

Span

📁 Source: Mathlib/Topology/Category/Profinite/Nobeling/Span.lean

Statistics

Metric	Count
Definitions `instFintypeElemForallBoolπMemFinset`, `spanFinBasis`, `πJ`	3
Theorems `finsuppSum_mem_span_eval`, `span`, `spanFin`, `e_mem_of_eq_true`, `eval_eq_πJ`, `factors_prod_eq_basis`, `factors_prod_eq_basis_of_eq`, `factors_prod_eq_basis_of_ne`, `fin_comap_jointlySurjective`, `list_prod_apply`, `one_sub_e_mem_of_false`, `span`	12
Total	15

Profinite.NobelingProof

Definitions

Name	Category	Theorems
`instFintypeElemForallBoolπMemFinset` 📖	CompOp	—
`spanFinBasis` 📖	CompOp	2 math math: `spanFinBasis.span`, `factors_prod_eq_basis`
`πJ` 📖	CompOp	1 math math: `eval_eq_πJ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`e_mem_of_eq_true` 📖	mathematical	`Set` `Set.instMembership` `π` `Finset` `Finset.instMembership` `Finset.decidableMem` `LinearOrder.toDecidableEq`	`LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Pi.topologicalSpace` `instTopologicalSpaceBool` `factors` `e`	—	`LE.total'`
`eval_eq_πJ` 📖	mathematical	`Products.isGood` `π` `Finset` `Finset.instMembership` `Finset.decidableMem` `LinearOrder.toDecidableEq`	`Products.eval` `DFunLike.coe` `LinearMap` `Int.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `LocallyConstant.instAddCommMonoid` `Int.instAddCommMonoid` `AddCommGroup.toIntModule` `LocallyConstant.instAddCommGroup` `Int.instAddCommGroup` `LinearMap.instFunLike` `πJ`	—	`LocallyConstant.ext` `Products.evalFacProp` `Products.prop_of_isGood`
`factors_prod_eq_basis` 📖	mathematical	—	`LocallyConstant` `Set.Elem` `π` `Finset` `Finset.instMembership` `Finset.decidableMem` `LinearOrder.toDecidableEq` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `LocallyConstant.instMul` `LocallyConstant.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `factors` `spanFinBasis`	—	`LocallyConstant.ext` `factors_prod_eq_basis_of_eq` `factors_prod_eq_basis_of_ne`
`factors_prod_eq_basis_of_eq` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `Set.Elem` `π` `Finset` `Finset.instMembership` `Finset.decidableMem` `LinearOrder.toDecidableEq` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `LocallyConstant.instFunLike` `LocallyConstant.instMul` `LocallyConstant.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `factors`	—	`list_prod_apply` `List.prod_eq_one` `LE.total'` `e.eq_1` `LocallyConstant.sub_apply` `LocallyConstant.isLocallyConstant` `sub_zero`
`factors_prod_eq_basis_of_ne` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `Set.Elem` `π` `Finset` `Finset.instMembership` `Finset.decidableMem` `LinearOrder.toDecidableEq` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `LocallyConstant.instFunLike` `LocallyConstant.instMul` `LocallyConstant.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `factors`	—	`list_prod_apply` `List.prod_eq_zero` `Mathlib.Tactic.Contrapose.contrapose₂` `one_sub_e_mem_of_false` `e.eq_1` `LocallyConstant.evalMonoidHom_apply` `LocallyConstant.sub_apply` `LocallyConstant.coe_one` `Pi.one_apply` `sub_self` `e_mem_of_eq_true`
`fin_comap_jointlySurjective` 📖	mathematical	—	`LocallyConstant.comap` `Set.Elem` `π` `Finset` `Finset.instMembership` `Finset.decidableMem` `LinearOrder.toDecidableEq` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `ProjRestrict` `continuous_projRestrict`	—	`IsClosed.isCompact` `Function.compactSpace` `Finite.compactSpace` `Bool.instFinite` `continuous_projRestrict` `Profinite.exists_locallyConstant` `CategoryTheory.isCofiltered_op_of_isFiltered` `CategoryTheory.isFiltered_of_directed_le_nonempty` `Finset.isDirected_le`
`list_prod_apply` 📖	mathematical	—	`DFunLike.coe` `LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `LocallyConstant.instFunLike` `LocallyConstant.instMul` `LocallyConstant.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `MonoidHom` `MulOneClass.toMulOne` `LocallyConstant.instMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `Int.instSemiring` `MonoidHom.instFunLike` `LocallyConstant.evalMonoidHom`	—	`map_list_prod` `MonoidHom.instMonoidHomClass` `LocallyConstant.evalMonoidHom_apply`
`one_sub_e_mem_of_false` 📖	mathematical	`Set` `Set.instMembership` `π` `Finset` `Finset.instMembership` `Finset.decidableMem` `LinearOrder.toDecidableEq`	`LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Pi.topologicalSpace` `instTopologicalSpaceBool` `factors` `LocallyConstant.instSub` `LocallyConstant.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Int.instRing` `e`	—	`LE.total'`

Profinite.NobelingProof.GoodProducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finsuppSum_mem_span_eval` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Set` `Profinite.NobelingProof.Products` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Int.instNormedCommRing` `setOf` `List.LE'`	`LocallyConstant` `Set.Elem` `Profinite.NobelingProof.π` `Finset.instMembership` `Finset.decidableMem` `LinearOrder.toDecidableEq` `instTopologicalSpaceSubtype` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `Submodule` `Int.instSemiring` `LocallyConstant.instAddCommMonoid` `Int.instAddCommMonoid` `AddCommGroup.toIntModule` `LocallyConstant.instAddCommGroup` `Int.instAddCommGroup` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Set.image` `Profinite.NobelingProof.Products.eval` `Finsupp.sum` `LocallyConstant.instMul` `Profinite.NobelingProof.e` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `LocallyConstant.instAddGroup` `Int.instAddGroup`	—	`Submodule.finsuppSum_mem` `Algebra.to_smulCommClass` `LinearMap.map_smul` `Submodule.smul_mem` `Submodule.subset_span` `List.IsChain.cons_of_le` `Subtype.prop` `List.cons_le_cons`
`span` 📖	mathematical	—	`Submodule` `LocallyConstant` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `Int.instSemiring` `LocallyConstant.instAddCommMonoid` `Int.instAddCommMonoid` `AddCommGroup.toIntModule` `LocallyConstant.instAddCommGroup` `Int.instAddCommGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range` `Profinite.NobelingProof.Products` `Profinite.NobelingProof.Products.isGood` `eval`	—	`span_iff_products` `Profinite.NobelingProof.fin_comap_jointlySurjective` `Submodule.span_mono` `Profinite.NobelingProof.eval_eq_πJ` `Subtype.prop` `Submodule.apply_mem_span_image_of_mem_span` `RingHomSurjective.ids` `spanFin` `Submodule.mem_top`
`spanFin` 📖	mathematical	—	`Submodule` `LocallyConstant` `Set.Elem` `Profinite.NobelingProof.π` `Finset` `Finset.instMembership` `Finset.decidableMem` `LinearOrder.toDecidableEq` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `Int.instSemiring` `LocallyConstant.instAddCommMonoid` `Int.instAddCommMonoid` `AddCommGroup.toIntModule` `LocallyConstant.instAddCommGroup` `Int.instAddCommGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range` `Profinite.NobelingProof.Products` `Profinite.NobelingProof.Products.isGood` `eval`	—	`span_iff_products` `le_trans` `Profinite.NobelingProof.spanFinBasis.span` `Submodule.span_le` `Profinite.NobelingProof.factors_prod_eq_basis` `instIsTransGe` `instAntisymmGe` `LE.total'` `List.sortedGT_iff_isChain` `Submodule.subset_span` `List.isChain_nil` `Finsupp.mem_span_image_iff_linearCombination` `List.isChain_cons` `Algebra.to_smulCommClass` `map_finsuppSum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `finsuppSum_mem_span_eval` `sub_eq_add_neg` `add_mul` `Distrib.rightDistribClass` `one_mul` `neg_mul` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.termg_eq` `add_zero` `one_zsmul` `Submodule.add_mem` `Submodule.finsuppSum_mem` `Submodule.smul_mem` `LT.lt.le` `le_of_lt` `List.lt_iff_lex_lt` `Submodule.span_mono` `Set.image_subset_range` `Finset.sortedGT_sort`

Profinite.NobelingProof.spanFinBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`span` 📖	mathematical	—	`Submodule` `LocallyConstant` `Set.Elem` `Profinite.NobelingProof.π` `Finset` `Finset.instMembership` `Finset.decidableMem` `LinearOrder.toDecidableEq` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `Pi.topologicalSpace` `instTopologicalSpaceBool` `Int.instSemiring` `LocallyConstant.instAddCommMonoid` `Int.instAddCommMonoid` `AddCommGroup.toIntModule` `LocallyConstant.instAddCommGroup` `Int.instAddCommGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Top.top` `Submodule.instTop` `Submodule.span` `Set.range` `Profinite.NobelingProof.spanFinBasis`	—	`Finsupp.mem_span_range_iff_exists_finsupp` `Finset.mem_univ` `LocallyConstant.ext` `zsmul_eq_mul` `map_finsuppSum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `mul_ite` `mul_one` `MulZeroClass.mul_zero` `Finsupp.sum_ite_eq`

---

← Back to Index