Ceva

📁 Source: Mathlib/Analysis/Normed/Affine/Ceva.lean

Statistics

Metric	Count
Definitions	0
Theorems prod_dist_div_dist_eq_one_of_mem_line_of_mem_line, prod_dist_eq_prod_dist_of_mem_line_of_mem_line	2
Total	2

Affine.Triangle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_dist_div_dist_eq_one_of_mem_line_of_mem_line 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Affine.Simplex.points Set.instSingletonSet	Finset.prod Real Real.instCommMonoid Finset.univ Fin.fintype DivInvMonoid.toDiv Real.instDivInvMonoid Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace Affine.Simplex.points NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddTorsor.toAddTorsor Real.instOne	—	prod_dist_eq_prod_dist_of_mem_line_of_mem_line Fin.prod_univ_three Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial
prod_dist_eq_prod_dist_of_mem_line_of_mem_line 📖	mathematical	AffineSubspace NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddTorsor.toAddTorsor SetLike.instMembership AffineSubspace.instSetLike affineSpan Set Set.instInsert Affine.Simplex.points Set.instSingletonSet	Finset.prod Real Real.instCommMonoid Finset.univ Fin.fintype Dist.dist PseudoMetricSpace.toDist Affine.Simplex.points NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing SeminormedAddCommGroup.toAddCommGroup NormedSpace.toModule NormedAddTorsor.toAddTorsor	—	Finset.prod_congr dist_lineMap_right dist_left_lineMap Finset.prod_mul_distrib NormedDivisionRing.toNormMulClass NormedDivisionRing.to_normOneClass prod_eq_prod_one_sub_of_mem_line_point_lineMap NormMulClass.toNoZeroDivisors

---

← Back to Index