Documentation Verification Report

StronglyRegular

📁 Source: Mathlib/Combinatorics/SimpleGraph/StronglyRegular.lean

Statistics

Metric	Count
Definitions `IsSRGWith`	1
Theorems `card`, `card_commonNeighbors_eq_of_adj_compl`, `card_commonNeighbors_eq_of_not_adj_compl`, `card_neighborFinset_union_eq`, `card_neighborFinset_union_of_adj`, `card_neighborFinset_union_of_not_adj`, `compl`, `compl_is_regular`, `matrix_eq`, `of_adj`, `of_not_adj`, `param_eq`, `regular`, `top`, `bot_strongly_regular`, `compl_neighborFinset_sdiff_inter_eq`, `sdiff_compl_neighborFinset_inter_eq`	17
Total	18

SimpleGraph

Definitions

Name	Category	Theorems
`IsSRGWith` 📖	CompData	2 math math: `IsSRGWith.top`, `bot_strongly_regular`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_strongly_regular` 📖	mathematical	—	`IsSRGWith` `Bot.bot` `SimpleGraph` `BooleanAlgebra.toBot` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `completeAtomicBooleanAlgebra` `Bot.adjDecidable` `Fintype.card`	—	`bot_degree` `Fintype.card_ofFinset` `Finset.ext`
`compl_neighborFinset_sdiff_inter_eq` 📖	mathematical	—	`Finset` `Finset.instInter` `Finset.instSDiff` `Compl.compl` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `neighborFinset` `neighborSetFintype` `Finset.instSingleton` `Finset.instUnion`	—	—
`sdiff_compl_neighborFinset_inter_eq` 📖	mathematical	`Adj`	`Finset` `Finset.instSDiff` `Finset.instInter` `Compl.compl` `BooleanAlgebra.toCompl` `Finset.booleanAlgebra` `neighborFinset` `neighborSetFintype` `Finset.instUnion` `Finset.instSingleton`	—	`adj_symm`

SimpleGraph.IsSRGWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card` 📖	mathematical	`SimpleGraph.IsSRGWith`	`Fintype.card`	—	—
`card_commonNeighbors_eq_of_adj_compl` 📖	mathematical	`SimpleGraph.IsSRGWith` `SimpleGraph.Adj` `Compl.compl` `SimpleGraph` `SimpleGraph.instCompl`	`Fintype.card` `Set.Elem` `SimpleGraph.commonNeighbors` `Subtype.fintype` `Set` `Set.instMembership` `SimpleGraph.decidableMemCommonNeighbors` `SimpleGraph.Compl.adjDecidable`	—	`Fintype.card_congr'` `SimpleGraph.neighborSet_compl` `Set.toFinset_inter` `Set.toFinset_diff` `Set.toFinset_compl` `Set.toFinset_singleton` `SimpleGraph.compl_neighborFinset_sdiff_inter_eq` `SimpleGraph.ne_of_adj` `Finset.card_sdiff_of_subset` `SimpleGraph.compl_adj` `Finset.insert_eq` `Finset.card_insert_of_notMem` `Finset.card_singleton` `Finset.compl_union` `Finset.card_compl` `card_neighborFinset_union_of_not_adj` `card`
`card_commonNeighbors_eq_of_not_adj_compl` 📖	mathematical	`SimpleGraph.IsSRGWith` `SimpleGraph.Adj` `Compl.compl` `SimpleGraph` `SimpleGraph.instCompl`	`Fintype.card` `Set.Elem` `SimpleGraph.commonNeighbors` `Subtype.fintype` `Set` `Set.instMembership` `SimpleGraph.decidableMemCommonNeighbors` `SimpleGraph.Compl.adjDecidable`	—	`Fintype.card_congr'` `SimpleGraph.neighborSet_compl` `Set.toFinset_inter` `Set.toFinset_diff` `Set.toFinset_compl` `Set.toFinset_singleton` `SimpleGraph.compl_neighborFinset_sdiff_inter_eq` `SimpleGraph.sdiff_compl_neighborFinset_inter_eq` `Finset.compl_union` `Finset.card_compl` `card_neighborFinset_union_of_adj` `card`
`card_neighborFinset_union_eq` 📖	mathematical	`SimpleGraph.IsSRGWith`	`Finset.card` `Finset` `Finset.instUnion` `SimpleGraph.neighborFinset` `SimpleGraph.neighborSetFintype` `Fintype.card` `Set.Elem` `SimpleGraph.commonNeighbors` `Subtype.fintype` `Set` `Set.instMembership` `SimpleGraph.decidableMemCommonNeighbors`	—	`le_trans` `SimpleGraph.card_commonNeighbors_le_degree_left` `SimpleGraph.IsRegularOfDegree.degree_eq` `regular` `two_mul` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.instCanonicallyOrderedAdd` `Set.toFinset_card` `Set.toFinset_inter` `Finset.card_union_add_card_inter`
`card_neighborFinset_union_of_adj` 📖	mathematical	`SimpleGraph.IsSRGWith` `SimpleGraph.Adj`	`Finset.card` `Finset` `Finset.instUnion` `SimpleGraph.neighborFinset` `SimpleGraph.neighborSetFintype`	—	`of_adj` `card_neighborFinset_union_eq`
`card_neighborFinset_union_of_not_adj` 📖	mathematical	`SimpleGraph.IsSRGWith` `SimpleGraph.Adj`	`Finset.card` `Finset` `Finset.instUnion` `SimpleGraph.neighborFinset` `SimpleGraph.neighborSetFintype`	—	`of_not_adj` `card_neighborFinset_union_eq`
`compl` 📖	mathematical	`SimpleGraph.IsSRGWith`	`Compl.compl` `SimpleGraph` `SimpleGraph.instCompl` `SimpleGraph.Compl.adjDecidable`	—	`card` `compl_is_regular` `card_commonNeighbors_eq_of_adj_compl` `card_commonNeighbors_eq_of_not_adj_compl`
`compl_is_regular` 📖	mathematical	`SimpleGraph.IsSRGWith`	`SimpleGraph.IsRegularOfDegree` `Compl.compl` `SimpleGraph` `SimpleGraph.instCompl` `SimpleGraph.neighborSetFintype` `SimpleGraph.Compl.adjDecidable`	—	`card` `add_comm` `SimpleGraph.IsRegularOfDegree.compl` `regular`
`matrix_eq` 📖	mathematical	`SimpleGraph.IsSRGWith`	`Matrix` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SimpleGraph.adjMatrix` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Matrix.add` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoid.toNatSMul` `Matrix.addMonoid` `AddMonoidWithOne.toAddMonoid` `Matrix.one` `Compl.compl` `SimpleGraph` `SimpleGraph.instCompl` `SimpleGraph.Compl.adjDecidable`	—	`Matrix.ext` `SimpleGraph.adjMatrix_pow_apply_eq_card_walk` `Fintype.card_congr` `eq_or_ne` `Set.toFinset_card` `Set.toFinset_congr` `Set.inter_self` `regular` `Matrix.one_apply_eq` `nsmul_eq_mul` `mul_one` `nsmul_zero` `add_zero` `Matrix.one_apply_ne'` `smul_zero` `zero_add` `of_adj` `of_not_adj`
`of_adj` 📖	mathematical	`SimpleGraph.IsSRGWith` `SimpleGraph.Adj`	`Fintype.card` `Set.Elem` `SimpleGraph.commonNeighbors` `Subtype.fintype` `Set` `Set.instMembership` `SimpleGraph.decidableMemCommonNeighbors`	—	—
`of_not_adj` 📖	mathematical	`SimpleGraph.IsSRGWith`	`Pairwise`	—	—
`param_eq` 📖	—	`SimpleGraph.IsSRGWith`	—	—	`Fintype.card_pos_iff` `card` `regular` `compl` `Finset.card_mul_eq_card_mul` `Finset.filter.congr_simp` `Finset.filter_mem_eq_inter` `Finset.singleton_subset_iff` `Finset.mem_sdiff` `SimpleGraph.mem_neighborFinset` `SimpleGraph.Adj.symm` `SimpleGraph.notMem_neighborFinset_self` `Finset.inter_comm` `SimpleGraph.neighborFinset_compl` `Finset.inter_sdiff_assoc` `Finset.sdiff_eq_inter_compl` `Finset.card_sdiff_of_subset` `Finset.card_singleton` `Finset.sdiff_inter_self_left` `Finset.inter_subset_left` `of_adj` `Set.toFinset_congr` `of_not_adj`
`regular` 📖	mathematical	`SimpleGraph.IsSRGWith`	`SimpleGraph.IsRegularOfDegree` `SimpleGraph.neighborSetFintype`	—	—
`top` 📖	mathematical	—	`SimpleGraph.IsSRGWith` `Top.top` `SimpleGraph` `BooleanAlgebra.toTop` `CompleteBooleanAlgebra.toBooleanAlgebra` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `SimpleGraph.completeAtomicBooleanAlgebra` `SimpleGraph.Top.adjDecidable` `Fintype.card`	—	`SimpleGraph.IsRegularOfDegree.top` `SimpleGraph.card_commonNeighbors_top` `SimpleGraph.top_adj`

---

← Back to Index