feat(LinearAlgebra/AffineSpace/Ceva): Ceva's theorem

[jsm28]

Add Ceva's theorem. Unlike various previous attempts, I think this in appropriate generality for mathlib; it starts with a version for an arbitary (possibly infinite) affinely independent family of points (not necessarily spanning the whole space), in any affine space over any ring, and with the second point given on each line not necessarily being on the opposite face, then deduces a simpler version for a finite family, then deduces versions for a triangle, now with actual cevians (lines between a vertex and a point on the opposite side), either just multiplying weights (here the ring requires no zero divisors) or expressed with a product of divisions equal to 1 (here it becomes a field).

This doesn't include any form of the converse (with a "concurrent or parallel" conclusion, and note that you don't need affine independence for the converse), or variants of the forward direction where you're given parallel lines rather than concurrent lines, but I think those things can reasonably be done in followups.

---

[github-actions]

PR summary c67909964b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.LinearAlgebra.AffineSpace.Ceva (new file)	844

---

Declarations diff

+ exists_affineCombination_eq_smul_eq
+ exists_affineCombination_eq_smul_eq_of_fintype
+ mem_affineSpan_pair_iff_exists_lineMap_eq
+ mem_affineSpan_pair_iff_exists_lineMap_rev_eq
+ prod_div_one_sub_eq_one_of_mem_line_point_lineMap
+ prod_eq_prod_one_sub_of_mem_line_point_lineMap

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[plby]

How does one decide the appropriate level of generality for Mathlib? What if prod_eq_prod_one_sub_of_mem_line_point_lineMap is true over an arbitrary ring, and prod_div_one_sub_eq_one_of_mem_line_point_lineMap over a division ring?

[jsm28]

Finset.prod requires a commutative monoid, so the statements for triangles don't even make sense without commutativity (and I didn't see any version of the statements for triangles that would be true in the noncommutative case even if you fix an order for the products).

I have however now done a slight generalization from IsDomain to NoZeroDivisors (i.e. allowing the case of the trivial ring, where the result is still (trivially) true but needs a different proof because of lemmas used in the main proof that require a nontrivial ring).

[jsm28]

As well as a version for a vector shared by the directions of the lines, and converses, other versions that might be reasonable for followups would be ones using dist in a NormedAddTorsor, ones using signedDist in a Euclidean space, and the angle form of Ceva in an oriented two-dimensional Euclidean space. But since the basic underlying results are purely affine, I think it makes sense to consider the affine versions the main ones and then build ones involving extra notions such as distance on top of them.

[plby]

(For the noncommutative case, see Theorem 4.2 here.)

Mostly I'm trying to get a feel for this concept of "appropriate generality for mathlib". I'm impressed that for "Ceva's theorem", that means something that doesn't include Ceva's theorem as stated by any result I get online, all of which use distances in Euclidean space.

[jsm28]

Theorem 4.2 there is explicitly described in the following sentence as "the Ceva’ theorem in the commutative case" (and despite the title of the following section there, I don't see anything actually claiming to be noncommutative Ceva; whereas the statements in this PR that aren't specific to triangles do work in the noncommutative case).

"appropriate generality for mathlib" would better be discussed on Zulip (with a view to someone writing up conclusions for a page on the community website) rather than in an individual PR. Specifically for Ceva only, an informal statement can talk about signed distances without trying to write down a precise definition of what a signed distance is, whereas in a formal context you can notice that "proportion of two signed distances on the same line" is a better-behaved, more-generally-meaningful concept than an individual signed distance in isolation, and a natural way to express such proportions in a formal statement that works in any affine space is to talk about points expressed using lineMap or affineCombination. There's nothing wrong with also having formal statements using dist, signedDist or oangle, but as a matter of formal library structure it's natural to derive those from the more general affine space versions using other lemmas about how lineMap relates to distances.

[jsm28]

And since 200 lines is plenty for one PR, it also makes sense to leave other versions for followups on the ground of keeping individual PRs small.

[plby]

(Sorry, I meant Theorem 4.13.)

[jsm28]

Theorem 4.13 there looks like a noncommutative version of Menelaus, not of Ceva. It does however suggest how it might be possible to produce a similar noncommutative version (stated with Fin.prod, I suppose, in order to get a noncommutative product) of Ceva for triangles (requiring division in an essential way, so only for DivisionRing not for Ring, so maybe requiring much of the proof of prod_eq_prod_one_sub_of_mem_line_point_lineMap to be duplicated with modifications since they are generalizing in different directions).