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 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	—	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