Documentation Verification Report

Configuration

📁 Source: Mathlib/Combinatorics/Configuration.lean

Statistics

Metric	Count
Definitions `hasLines`, `hasPoints`, `HasLines`, `hasPoints`, `mkLine`, `HasPoints`, `hasLines`, `mkPoint`, `ProjectivePlane`, `instDual`, `mkLine`, `toHasLines`, `toHasPoints`, `instFintypeDual`, `instInhabitedDual`, `instMembershipDual`, `lineCount`, `instMembershipProjectivizationForallFinOfNatNat`, `instProjectivePlaneProjectivizationForallFinOfNatNatOfDecidableEq`, `pointCount`	20
Theorems `card_le`, `existsUnique_line`, `exists_bijective_of_card_eq`, `lineCount_eq_pointCount`, `mkLine_ax`, `pointCount_le_lineCount`, `toNondegenerate`, `card_le`, `existsUnique_point`, `lineCount_eq_pointCount`, `lineCount_le_pointCount`, `mkPoint_ax`, `toNondegenerate`, `eq_or_eq`, `exists_injective_of_card_le`, `exists_line`, `exists_point`, `card_lines`, `card_points`, `card_points_eq_card_lines`, `exists_config`, `lineCount_eq`, `lineCount_eq_lineCount`, `lineCount_eq_pointCount`, `mkLine_ax`, `one_lt_order`, `pointCount_eq`, `pointCount_eq_pointCount`, `two_lt_lineCount`, `two_lt_pointCount`, `instFiniteDual`, `crossProduct_eq_zero_of_dotProduct_eq_zero`, `eq_or_eq_of_orthogonal`, `instNondegenerateProjectivizationForallFinOfNatNat`, `mem_iff`, `sum_lineCount_eq_sum_pointCount`	36
Total	56

Configuration

Definitions

Name	Category	Theorems
`HasLines` 📖	CompData	—
`HasPoints` 📖	CompData	—
`ProjectivePlane` 📖	CompData	—
`instFintypeDual` 📖	CompOp	—
`instInhabitedDual` 📖	CompOp	—
`instMembershipDual` 📖	CompOp	2 math math: `Dual.Nondegenerate`, `ProjectivePlane.Dual.order`
`lineCount` 📖	CompOp	10 math math: `ProjectivePlane.lineCount_eq_lineCount`, `ProjectivePlane.two_lt_lineCount`, `HasPoints.lineCount_le_pointCount`, `HasLines.pointCount_le_lineCount`, `sum_lineCount_eq_sum_pointCount`, `ProjectivePlane.lineCount_eq`, `ProjectivePlane.lineCount_eq_pointCount`, `HasLines.exists_bijective_of_card_eq`, `HasLines.lineCount_eq_pointCount`, `HasPoints.lineCount_eq_pointCount`
`pointCount` 📖	CompOp	10 math math: `ProjectivePlane.two_lt_pointCount`, `HasPoints.lineCount_le_pointCount`, `HasLines.pointCount_le_lineCount`, `sum_lineCount_eq_sum_pointCount`, `ProjectivePlane.lineCount_eq_pointCount`, `HasLines.exists_bijective_of_card_eq`, `HasLines.lineCount_eq_pointCount`, `ProjectivePlane.pointCount_eq_pointCount`, `ProjectivePlane.pointCount_eq`, `HasPoints.lineCount_eq_pointCount`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteDual` 📖	mathematical	—	`Finite` `Dual`	—	—
`sum_lineCount_eq_sum_pointCount` 📖	mathematical	—	`Finset.sum` `Nat.instAddCommMonoid` `Finset.univ` `lineCount` `pointCount`	—	`Finset.sum_congr` `Nat.card_eq_fintype_card` `Fintype.card_congr`

Configuration.Dual

Definitions

Name	Category	Theorems
`hasLines` 📖	CompOp	—
`hasPoints` 📖	CompOp	—

Configuration.HasLines

Definitions

Name	Category	Theorems
`hasPoints` 📖	CompOp	—
`mkLine` 📖	CompOp	1 math math: `mkLine_ax`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le` 📖	mathematical	—	`Fintype.card`	—	`Configuration.Nondegenerate.exists_injective_of_card_le` `toNondegenerate` `le_of_not_ge` `Configuration.sum_lineCount_eq_sum_pointCount` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `pointCount_le_lineCount` `Subtype.finite` `Finite.of_fintype` `Finset.sum_map` `Fintype.card_le_of_surjective` `Finset.sum_lt_sum_of_subset` `Nat.instIsOrderedCancelAddMonoid` `Finset.subset_univ` `Finset.mem_univ` `Configuration.lineCount.eq_1` `Nat.card_eq_fintype_card` `Fintype.card_pos_iff` `Configuration.Nondegenerate.exists_line` `mkLine_ax` `zero_le` `Nat.instCanonicallyOrderedAdd` `lt_irrefl`
`existsUnique_line` 📖	mathematical	—	`ExistsUnique`	—	`Configuration.HasPoints.existsUnique_point`
`exists_bijective_of_card_eq` 📖	mathematical	`Fintype.card`	`Function.Bijective` `Configuration.pointCount` `Configuration.lineCount`	—	`Configuration.Nondegenerate.exists_injective_of_card_le` `toNondegenerate` `ge_of_eq` `Fintype.bijective_iff_injective_and_card` `Finset.sum_eq_sum_iff_of_le` `Nat.instIsOrderedCancelAddMonoid` `pointCount_le_lineCount` `Subtype.finite` `Finite.of_fintype` `Function.Bijective.sum_comp` `Configuration.sum_lineCount_eq_sum_pointCount` `Finset.mem_univ`
`lineCount_eq_pointCount` 📖	mathematical	`Fintype.card`	`Configuration.lineCount` `Configuration.pointCount`	—	`exists_bijective_of_card_eq` `Finset.univ_product_univ` `Finset.sum_product_right` `Finset.sum_product` `Finset.sum_congr` `Finset.sum_const` `Configuration.sum_lineCount_eq_sum_pointCount` `Finset.sum_finset_product` `Finset.sum_finset_product_right` `Finset.sum_bijective` `Set.toFinset_card` `add_left_cancel_iff` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Finset.sum_add_sum_compl` `Finset.sum_eq_sum_iff_of_le` `Nat.instIsOrderedCancelAddMonoid` `pointCount_le_lineCount` `Set.mem_toFinset` `Subtype.finite` `Finite.of_fintype` `Set.toFinset_compl`
`mkLine_ax` 📖	mathematical	—	`mkLine`	—	—
`pointCount_le_lineCount` 📖	mathematical	—	`Configuration.pointCount` `Configuration.lineCount`	—	`LE.le.trans` `le_of_eq` `Nat.card_eq_zero_of_infinite` `zero_le` `Nat.instCanonicallyOrderedAdd` `nonempty_fintype` `Configuration.lineCount.eq_1` `Configuration.pointCount.eq_1` `Nat.card_eq_fintype_card` `Fintype.card_le_of_injective` `mkLine_ax` `Configuration.Nondegenerate.eq_or_eq` `toNondegenerate`
`toNondegenerate` 📖	mathematical	—	`Configuration.Nondegenerate`	—	—

Configuration.HasPoints

Definitions

Name	Category	Theorems
`hasLines` 📖	CompOp	—
`mkPoint` 📖	CompOp	1 math math: `mkPoint_ax`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le` 📖	mathematical	—	`Fintype.card`	—	`Configuration.HasLines.card_le`
`existsUnique_point` 📖	mathematical	—	`ExistsUnique`	—	`mkPoint_ax` `Configuration.Nondegenerate.eq_or_eq` `toNondegenerate`
`lineCount_eq_pointCount` 📖	mathematical	`Fintype.card`	`Configuration.lineCount` `Configuration.pointCount`	—	`Configuration.HasLines.lineCount_eq_pointCount`
`lineCount_le_pointCount` 📖	mathematical	—	`Configuration.lineCount` `Configuration.pointCount`	—	`Configuration.HasLines.pointCount_le_lineCount`
`mkPoint_ax` 📖	mathematical	—	`mkPoint`	—	—
`toNondegenerate` 📖	mathematical	—	`Configuration.Nondegenerate`	—	—

Configuration.Nondegenerate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_or_eq` 📖	—	—	—	—	—
`exists_injective_of_card_le` 📖	—	`Fintype.card`	—	—	`Nat.instCanonicallyOrderedAdd` `Finset.card_eq_one` `exists_point` `Finset.card_singleton` `Finset.singleton_biUnion` `Finset.card_ne_zero_of_mem` `Set.mem_toFinset` `Finset.card_le_one_iff` `Finset.one_lt_card_iff` `eq_or_eq` `Finset.card_compl` `tsub_eq_zero_iff_le` `Nat.instOrderedSub` `LE.le.ge_iff_eq'` `Finset.card_le_univ` `Finset.card_eq_iff_eq_univ` `Finset.eq_univ_iff_forall` `exists_line` `Finset.mem_biUnion` `Finset.mem_univ` `LE.le.trans` `tsub_le_iff_left` `add_le_add_iff_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `le_tsub_iff_left` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `le_add_left` `add_tsub_assoc_of_le` `Finset.all_card_le_biUnion_card_iff_exists_injective`
`exists_line` 📖	—	—	—	—	—
`exists_point` 📖	—	—	—	—	—

Configuration.ProjectivePlane

Definitions

Name	Category	Theorems
`instDual` 📖	CompOp	1 math math: `Dual.order`
`mkLine` 📖	CompOp	1 math math: `mkLine_ax`
`toHasLines` 📖	CompOp	—
`toHasPoints` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_lines` 📖	mathematical	—	`Fintype.card` `Monoid.toNatPow` `Nat.instMonoid` `order`	—	`card_points` `Configuration.instFiniteDual` `Dual.order` `Finite.of_fintype`
`card_points` 📖	mathematical	—	`Fintype.card` `Monoid.toNatPow` `Nat.instMonoid` `order`	—	`nonempty_fintype` `exists_config` `mkLine_ax` `Sigma.subtype_ext` `Configuration.Nondegenerate.eq_or_eq` `Configuration.HasLines.toNondegenerate` `eq_tsub_iff_add_eq_of_le` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Fintype.card_pos_iff` `Fintype.card_subtype_compl` `Fintype.card_subtype_eq` `Fintype.card_congr` `Nat.card_eq_fintype_card` `tsub_eq_of_eq_add` `pointCount_eq` `Finite.of_fintype` `Fintype.card_congr'` `Fintype.card_sigma` `Finset.sum_congr` `Finset.sum_const` `Configuration.lineCount.eq_1` `lineCount_eq` `smul_eq_mul` `sq`
`card_points_eq_card_lines` 📖	mathematical	—	`Fintype.card`	—	`le_antisymm` `Configuration.HasLines.card_le` `Configuration.HasPoints.card_le`
`exists_config` 📖	—	—	—	—	—
`lineCount_eq` 📖	mathematical	—	`Configuration.lineCount` `order`	—	`exists_config` `nonempty_fintype` `Subtype.finite` `order.eq_1` `lineCount_eq_lineCount` `Configuration.lineCount.eq_1` `Nat.card_eq_fintype_card` `Fintype.card_pos_iff`
`lineCount_eq_lineCount` 📖	mathematical	—	`Configuration.lineCount`	—	`nonempty_fintype` `exists_config` `card_points_eq_card_lines` `Configuration.HasLines.lineCount_eq_pointCount` `or_not` `Configuration.Nondegenerate.eq_or_eq` `Configuration.HasLines.toNondegenerate`
`lineCount_eq_pointCount` 📖	mathematical	—	`Configuration.lineCount` `Configuration.pointCount`	—	`Configuration.Nondegenerate.exists_point` `Configuration.HasLines.toNondegenerate` `lineCount_eq_lineCount` `nonempty_fintype` `Configuration.HasLines.lineCount_eq_pointCount` `card_points_eq_card_lines`
`mkLine_ax` 📖	mathematical	—	`mkLine`	—	—
`one_lt_order` 📖	mathematical	—	`order`	—	`exists_config` `nonempty_fintype` `Subtype.finite` `add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `pointCount_eq` `Configuration.pointCount.eq_1` `Nat.card_eq_fintype_card` `Fintype.two_lt_card_iff` `Configuration.HasPoints.mkPoint_ax`
`pointCount_eq` 📖	mathematical	—	`Configuration.pointCount` `order`	—	`lineCount_eq` `Configuration.instFiniteDual` `Dual.order`
`pointCount_eq_pointCount` 📖	mathematical	—	`Configuration.pointCount`	—	`lineCount_eq_lineCount` `Configuration.instFiniteDual`
`two_lt_lineCount` 📖	mathematical	—	`Configuration.lineCount`	—	`lineCount_eq` `one_lt_order`
`two_lt_pointCount` 📖	mathematical	—	`Configuration.pointCount`	—	`pointCount_eq` `one_lt_order`

Configuration.ofField

Definitions

Name	Category	Theorems
`instMembershipProjectivizationForallFinOfNatNat` 📖	CompOp	2 math math: `instNondegenerateProjectivizationForallFinOfNatNat`, `mem_iff`
`instProjectivePlaneProjectivizationForallFinOfNatNatOfDecidableEq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`crossProduct_eq_zero_of_dotProduct_eq_zero` 📖	mathematical	`dotProduct` `Fin.fintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `NonUnitalNonAssocSemiring.toAddCommMonoid` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `Pi.Function.module` `Semiring.toModule` `LinearMap.instFunLike` `LinearMap.addCommMonoid` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `crossProduct` `Pi.instZero`	—	`Function.smulCommClass` `Algebra.to_smulCommClass` `Matrix.ext` `Fintype.complete` `Matrix.rank_add_rank_le_card_of_mul_eq_zero` `Finite.of_fintype` `Fintype.card_fin` `LinearIndependent.rank_matrix` `Matrix.of_row` `Matrix.rank_transpose`
`eq_or_eq_of_orthogonal` 📖	—	`Projectivization.orthogonal` `Fin.fintype`	—	—	`Projectivization.ind` `Function.smulCommClass` `Algebra.to_smulCommClass` `Projectivization.mk_eq_mk_iff_crossProduct_eq_zero` `crossProduct_eq_zero_of_dotProduct_eq_zero`
`instNondegenerateProjectivizationForallFinOfNatNat` 📖	mathematical	—	`Configuration.Nondegenerate` `Projectivization` `Field.toDivisionRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Pi.Function.module` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `instMembershipProjectivizationForallFinOfNatNat`	—	`Projectivization.exists_not_orthogonal_self` `Projectivization.exists_not_self_orthogonal` `eq_or_eq_of_orthogonal`
`mem_iff` 📖	mathematical	—	`Projectivization` `Field.toDivisionRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `DivisionRing.toRing` `Pi.Function.module` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Ring.toSemiring` `Semiring.toModule` `instMembershipProjectivizationForallFinOfNatNat` `Projectivization.orthogonal` `Fin.fintype`	—	—

---

← Back to Index