DotProduct

📁 Source: Mathlib/LinearAlgebra/Matrix/DotProduct.lean

Statistics

Metric	Count
Definitions	0
Theorems conjTranspose_mul_self_eq_zero, conjTranspose_mul_self_mulVec_eq_zero, conjTranspose_mul_self_mul_eq_zero, dotProduct_self_star_pos_iff, dotProduct_star_self_pos_iff, mul_conjTranspose_mul_self_eq_zero, mul_self_mul_conjTranspose_eq_zero, self_mul_conjTranspose_eq_zero, self_mul_conjTranspose_mulVec_eq_zero, self_mul_conjTranspose_mul_eq_zero, vecMul_conjTranspose_mul_self_eq_zero, vecMul_self_mul_conjTranspose_eq_zero, dotProduct_eq, dotProduct_eq_iff, dotProduct_eq_zero, dotProduct_eq_zero_iff, dotProduct_le_dotProduct_of_nonneg_left, dotProduct_le_dotProduct_of_nonneg_right, dotProduct_nonneg_of_nonneg, dotProduct_self_eq_zero, dotProduct_self_star_eq_zero, dotProduct_self_star_nonneg, dotProduct_star_self_eq_zero, dotProduct_star_self_nonneg	24
Total	24

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjTranspose_mul_self_eq_zero 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	ext dotProduct_star_self_eq_zero ext_iff mul_zero
conjTranspose_mul_self_mulVec_eq_zero 📖	mathematical	—	mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	conjTranspose_mul_self_mul_eq_zero
conjTranspose_mul_self_mul_eq_zero 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	conjTranspose_mul_self_eq_zero conjTranspose_mul mul_assoc mul_zero
dotProduct_self_star_pos_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid	—	star_star dotProduct_star_self_pos_iff
dotProduct_star_self_pos_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Fintype.sum_pos_iff_of_nonneg IsOrderedAddMonoid.toIsOrderedCancelAddMonoid IsOrderedCancelAddMonoid.toIsOrderedAddMonoid StarOrderedRing.toIsOrderedAddMonoid star_mul_self_nonneg star_zero MulZeroClass.mul_zero star_mul_self_pos IsRegular.of_ne_zero NoZeroDivisors.to_isCancelMulZero
mul_conjTranspose_mul_self_eq_zero 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	conjTranspose_conjTranspose mul_self_mul_conjTranspose_eq_zero
mul_self_mul_conjTranspose_eq_zero 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	conjTranspose_eq_zero conjTranspose_mul conjTranspose_conjTranspose self_mul_conjTranspose_mul_eq_zero
self_mul_conjTranspose_eq_zero 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	ext dotProduct_self_star_eq_zero ext_iff zero_mul
self_mul_conjTranspose_mulVec_eq_zero 📖	mathematical	—	mulVec NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	conjTranspose_conjTranspose conjTranspose_mul_self_mulVec_eq_zero
self_mul_conjTranspose_mul_eq_zero 📖	mathematical	—	Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	conjTranspose_conjTranspose conjTranspose_mul_self_mul_eq_zero
vecMul_conjTranspose_mul_self_eq_zero 📖	mathematical	—	vecMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	mul_conjTranspose_mul_self_eq_zero
vecMul_self_mul_conjTranspose_eq_zero 📖	mathematical	—	vecMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing Matrix instHMulOfFintypeOfMulOfAddCommMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid conjTranspose InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	conjTranspose_conjTranspose vecMul_conjTranspose_mul_self_eq_zero

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dotProduct_eq 📖	—	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid	—	—	dotProduct_single_one
dotProduct_eq_iff 📖	mathematical	—	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid	—	dotProduct_eq
dotProduct_eq_zero 📖	mathematical	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Pi.instZero	—	dotProduct_eq zero_dotProduct
dotProduct_eq_zero_iff 📖	mathematical	—	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Pi.instZero	—	dotProduct_eq_zero zero_dotProduct
dotProduct_le_dotProduct_of_nonneg_left 📖	mathematical	Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid	—	Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono
dotProduct_le_dotProduct_of_nonneg_right 📖	mathematical	Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid	—	Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono
dotProduct_nonneg_of_nonneg 📖	mathematical	Pi.hasLe Preorder.toLE PartialOrder.toPreorder Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid	—	Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid mul_nonneg IsOrderedRing.toPosMulMono
dotProduct_self_eq_zero 📖	mathematical	—	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Pi.instZero	—	Finset.sum_eq_zero_iff_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing mul_self_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono IsStrictOrderedRing.noZeroDivisors
dotProduct_self_star_eq_zero 📖	mathematical	—	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Pi.instZero	—	Fintype.sum_eq_zero_iff_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid mul_star_self_nonneg
dotProduct_self_star_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid	—	Fintype.sum_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid mul_star_self_nonneg
dotProduct_star_self_eq_zero 📖	mathematical	—	dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNonAssocSemiring.toAddCommMonoid Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Pi.instZero	—	Fintype.sum_eq_zero_iff_of_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid star_mul_self_nonneg
dotProduct_star_self_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocSemiring.toAddCommMonoid Star.star Pi.instStarForall InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid	—	Fintype.sum_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid star_mul_self_nonneg

---

← Back to Index