Affine

📁 Source: Mathlib/Analysis/InnerProductSpace/Affine.lean

Statistics

Metric	Count
Definitions	0
Theorems dist_sq_lineMap_lineMap_of_inner_eq_zero, dist_sq_lineMap_of_inner_eq_zero, dist_sq_of_inner_eq_zero, inner_vsub_left_eq_zero_symm, inner_vsub_right_eq_zero_symm, inner_vsub_vsub_left_eq_dist_sq_left_iff, inner_vsub_vsub_left_eq_dist_sq_right_iff, inner_vsub_vsub_right_eq_dist_sq_left_iff, inner_vsub_vsub_right_eq_dist_sq_right_iff	9
Total	9

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_sq_lineMap_lineMap_of_inner_eq_zero 📖	mathematical	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real.instZero	Monoid.toNatPow Real.instMonoid Dist.dist PseudoMetricSpace.toDist DFunLike.coe AffineMap Real.instRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace AffineMap.instFunLike AffineMap.lineMap Real.instAdd Real.instMul	—	AffineMap.lineMap_apply vadd_vsub_vadd_cancel_right dist_eq_norm_vsub Nat.instAtLeastTwoHAddOfNat norm_sub_sq_real norm_smul NormedSpace.toNormSMulClass Real.norm_eq_abs inner_smul_left inner_smul_right dist_eq_norm_vsub' mul_pow sq_abs MulZeroClass.mul_zero sub_zero
dist_sq_lineMap_of_inner_eq_zero 📖	mathematical	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real.instZero	Monoid.toNatPow Real.instMonoid Dist.dist PseudoMetricSpace.toDist DFunLike.coe AffineMap Real.instRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring addGroupIsAddTorsor AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne NormedAddCommGroup.toAddCommGroup NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace AffineMap.instFunLike AffineMap.lineMap Real.instAdd Real.instMul	—	dist_sq_lineMap_lineMap_of_inner_eq_zero dist_comm AffineMap.lineMap_apply_one one_pow one_mul
dist_sq_of_inner_eq_zero 📖	mathematical	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Real.instZero	Monoid.toNatPow Real.instMonoid Dist.dist PseudoMetricSpace.toDist Real.instAdd	—	AffineMap.lineMap_apply_one one_pow one_mul dist_sq_lineMap_of_inner_eq_zero
inner_vsub_left_eq_zero_symm 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	neg_vsub_eq_vsub_rev inner_neg_left neg_eq_zero
inner_vsub_right_eq_zero_symm 📖	mathematical	—	Inner.inner InnerProductSpace.toInner NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField	—	neg_vsub_eq_vsub_rev inner_neg_right neg_eq_zero
inner_vsub_vsub_left_eq_dist_sq_left_iff 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Monoid.toNatPow Real.instMonoid Dist.dist PseudoMetricSpace.toDist Real.instZero	—	dist_eq_norm_vsub inner_eq_norm_sq_left_iff vsub_sub_vsub_cancel_left inner_vsub_right_eq_zero_symm
inner_vsub_vsub_left_eq_dist_sq_right_iff 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Monoid.toNatPow Real.instMonoid Dist.dist PseudoMetricSpace.toDist Real.instZero	—	real_inner_comm inner_vsub_vsub_left_eq_dist_sq_left_iff
inner_vsub_vsub_right_eq_dist_sq_left_iff 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Monoid.toNatPow Real.instMonoid Dist.dist PseudoMetricSpace.toDist Real.instZero	—	dist_eq_norm_vsub inner_eq_norm_sq_left_iff vsub_sub_vsub_cancel_right inner_vsub_right_eq_zero_symm
inner_vsub_vsub_right_eq_dist_sq_right_iff 📖	mathematical	—	Inner.inner Real InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup VSub.vsub AddTorsor.toVSub SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup NormedAddTorsor.toAddTorsor MetricSpace.toPseudoMetricSpace Monoid.toNatPow Real.instMonoid Dist.dist PseudoMetricSpace.toDist Real.instZero	—	real_inner_comm inner_vsub_vsub_right_eq_dist_sq_left_iff

---

← Back to Index