Basic

📁 Source: Mathlib/Geometry/Euclidean/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems dist_affineCombination, dist_smul_vadd_eq_dist, dist_smul_vadd_sq, eq_of_dist_eq_of_dist_eq_of_finrank_eq_two, eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two, inner_weightedVSub	6
Total	6

EuclideanGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_affineCombination 📖	mathematical	Finset.sum Real Real.instAddCommMonoid Real.instOne	Real.instMul Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace DFunLike.coe AffineMap Real.instRing Pi.addCommGroup Ring.toAddCommGroup Pi.Function.module Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Semiring.toModule Finset.instAddTorsorForall NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddTorsor.toAddTorsor AffineMap.instFunLike Finset.affineCombination DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Pi.instSub Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat dist_eq_norm_vsub inner_self_eq_norm_mul_norm Finset.affineCombination_vsub Finset.sum_congr Finset.sum_sub_distrib sub_self inner_weightedVSub
dist_smul_vadd_eq_dist 📖	mathematical	—	Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NormedAddTorsor.toAddTorsor Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.instZero DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Inner.inner InnerProductSpace.toInner VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	Nat.instAtLeastTwoHAddOfNat mul_self_inj_of_nonneg NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Real.instIsStrictOrderedRing dist_nonneg dist_smul_vadd_sq mul_assoc sub_eq_zero add_sub_assoc dist_eq_norm_vsub real_inner_self_eq_norm_mul_norm sub_self inner_self_eq_norm_sq_to_K isReduced_of_noZeroDivisors Nat.instCharZero discrim.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_mul quadratic_eq_zero_iff CharZero.NeZero.two RCLike.charZero_rclike neg_add_cancel zero_div neg_mul_eq_neg_mul mul_sub_right_distrib sub_eq_add_neg mul_two mul_div_assoc mul_div_mul_left
dist_smul_vadd_sq 📖	mathematical	—	Real Real.instMul Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace HVAdd.hVAdd instHVAdd AddSemigroupAction.toVAdd AddMonoid.toAddSemigroup ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid AddAction.toAddSemigroupAction AddTorsor.toAddAction NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NormedAddTorsor.toAddTorsor SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Real.instAdd Inner.inner InnerProductSpace.toInner instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	Nat.instAtLeastTwoHAddOfNat dist_eq_norm_vsub real_inner_self_eq_norm_mul_norm vadd_vsub_assoc real_inner_add_add_self real_inner_smul_left real_inner_smul_right Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
eq_of_dist_eq_of_dist_eq_of_finrank_eq_two 📖	—	Module.finrank Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	—	—	eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two FiniteDimensional.finiteDimensional_submodule AffineSubspace.direction_top finrank_top AffineSubspace.mem_top
eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two 📖	—	Module.finrank Real Submodule Ring.toSemiring Real.instRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField NormedAddCommGroup.toSeminormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike SetLike.instMembership Submodule.setLike AffineSubspace.direction NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real.semiring Submodule.addCommMonoid Submodule.module AffineSubspace AffineSubspace.instSetLike Dist.dist PseudoMetricSpace.toDist	—	—	inner_vsub_vsub_of_dist_eq_of_dist_eq linearIndependent_of_ne_zero_of_inner_eq_zero Fintype.complete Matrix.cons_val_fin_one real_inner_comm Submodule.eq_of_le_of_finrank_eq Submodule.span_le Set.range_subset_iff AffineSubspace.vsub_mem_direction finrank_span_eq_card IsNoetherianRing.strongRankCondition Real.instNontrivial PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain Fintype.card_fin Fintype.coe_image_univ Finset.image_insert Finset.image_singleton Finset.coe_insert Finset.coe_singleton Submodule.mem_span_insert Submodule.mem_span_singleton one_smul vsub_vadd Nat.instAtLeastTwoHAddOfNat NeZero.charZero_one RCLike.charZero_rclike dist_smul_vadd_eq_dist zero_smul zero_vadd eq_vadd_iff_vsub_eq zero_add inner_add_right inner_smul_right MulZeroClass.mul_zero add_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
inner_weightedVSub 📖	mathematical	Finset.sum Real Real.instAddCommMonoid Real.instZero	Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup DFunLike.coe LinearMap Ring.toSemiring Real.instRing RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid NormedAddCommGroup.toAddCommGroup Pi.Function.module Semiring.toModule NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace LinearMap.instFunLike Finset.weightedVSub NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instNeg Real.instMul Dist.dist PseudoMetricSpace.toDist instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat AddTorsor.nonempty Finset.weightedVSub_apply inner_sum_smul_sum_smul_of_sum_eq_zero Finset.sum_congr vsub_sub_vsub_cancel_right dist_eq_norm_vsub

---

← Back to Index