Documentation Verification Report

Ceva

📁 Source: Mathlib/LinearAlgebra/AffineSpace/Ceva.lean

Statistics

Metric	Count
Definitions	0
Theorems `prod_div_one_sub_eq_one_of_mem_line_point_lineMap`, `prod_eq_prod_one_sub_of_mem_line_point_lineMap`, `exists_affineCombination_eq_smul_eq`, `exists_affineCombination_eq_smul_eq_of_fintype`	4
Total	4

Affine.Triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_div_one_sub_eq_one_of_mem_line_point_lineMap` 📖	mathematical	`AffineSubspace` `DivisionRing.toRing` `Field.toDivisionRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Affine.Simplex.points` `Set.instSingletonSet` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	`Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `Finset.univ` `Fin.fintype` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`Finset.prod_div_distrib` `prod_eq_prod_one_sub_of_mem_line_point_lineMap` `IsDomain.to_noZeroDivisors` `Field.isDomain` `div_self` `Finset.prod_ne_zero_iff` `DivisionRing.toNontrivial`
`prod_eq_prod_one_sub_of_mem_line_point_lineMap` 📖	mathematical	`AffineSubspace` `CommRing.toRing` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Affine.Simplex.points` `Set.instSingletonSet` `DFunLike.coe` `AffineMap` `Ring.toAddCommGroup` `Semiring.toModule` `Ring.toSemiring` `addGroupIsAddTorsor` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AffineMap.instFunLike` `AffineMap.lineMap`	`Finset.prod` `CommRing.toCommMonoid` `Finset.univ` `Fin.fintype` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`subsingleton_or_nontrivial` `Finset.sum_congr` `Finset.sum_affineCombinationLineMapWeights` `Finset.affineCombination_affineCombinationLineMapWeights` `AffineIndependent.exists_affineCombination_eq_smul_eq_of_fintype` `Affine.Simplex.independent` `Set.indicator_of_mem` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Finset.affineCombinationLineMapWeights_apply_left` `Finset.affineCombinationLineMapWeights_apply_right` `Finset.prod_congr` `Finset.prod_comp_equiv` `Finset.univ_map_embedding` `Finset.prod_eq_zero_iff` `MulZeroClass.zero_mul` `Fin.sum_univ_three` `Fintype.complete` `add_assoc` `add_zero` `mul_add` `Distrib.leftDistribClass` `add_sub_cancel` `mul_one` `one_mul` `zero_add` `Finset.prod_eq_zero` `sub_self` `mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `NoZeroDivisors.to_isCancelMulZero`

AffineIndependent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_affineCombination_eq_smul_eq` 📖	mathematical	`AffineIndependent` `Set.Nonempty` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instMembership` `Set.instSingletonSet` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Set.indicator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Set.instSDiff` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`Finset.sum_congr` `Finset.insert_eq_of_mem` `Set.indicator_of_mem` `Finset.sum_insert` `Set.indicator_of_notMem` `zero_add` `Finset.affineCombination_indicator_subset` `Set.indicator_apply` `Finset.coe_insert` `Set.insert_diff_of_mem`
`exists_affineCombination_eq_smul_eq_of_fintype` 📖	mathematical	`AffineIndependent` `Set.Nonempty` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.univ` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AffineSubspace` `SetLike.instMembership` `AffineSubspace.instSetLike` `affineSpan` `Set` `Set.instInsert` `Set.instMembership` `Set.instSingletonSet` `DFunLike.coe` `AffineMap` `Pi.addCommGroup` `Ring.toAddCommGroup` `Pi.Function.module` `Ring.toSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `Semiring.toModule` `Finset.instAddTorsorForall` `AffineMap.instFunLike` `Finset.affineCombination`	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Set.indicator` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `Compl.compl` `Set.instCompl`	—	`exists_affineCombination_eq_smul_eq` `Finset.sum_indicator_subset` `Finset.affineCombination_indicator_subset` `Set.indicator_apply` `mul_ite` `MulZeroClass.mul_zero` `Finset.coe_univ` `Set.indicator_of_notMem` `Set.indicator_of_mem`

---

← Back to Index