Vec

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

Statistics

Metric	Count
Definitions `vec`, `Vec`, `Vec`	3
Theorems `kronecker_mulVec_vec`, `kronecker_mulVec_vec_of_commute`, `star_vec`, `star_vec_dotProduct_vec`, `vec_add`, `vec_bijective`, `vec_dotProduct_vec`, `vec_eq_uncurry`, `vec_eq_zero_iff`, `vec_hadamard`, `vec_inj`, `vec_map`, `vec_mul_eq_mulVec`, `vec_mul_eq_vecMul`, `vec_neg`, `vec_of`, `vec_single`, `vec_smul`, `vec_sub`, `vec_sum`, `vec_transpose`, `vec_vecMul_kronecker`, `vec_vecMul_kronecker_of_commute`, `vec_zero`	24
Total	27

Matrix

Definitions

Name	Category	Theorems
`vec` 📖	CompOp	24 math math: `vec_add`, `vec_sum`, `vec_neg`, `star_vec`, `vec_of`, `star_vec_dotProduct_vec`, `vec_dotProduct_vec`, `vec_transpose`, `vec_hadamard`, `vec_sub`, `vec_smul`, `vec_single`, `vec_inj`, `vec_eq_zero_iff`, `vec_vecMul_kronecker_of_commute`, `vec_zero`, `vec_vecMul_kronecker`, `kronecker_mulVec_vec`, `vec_mul_eq_vecMul`, `vec_mul_eq_mulVec`, `kronecker_mulVec_vec_of_commute`, `vec_map`, `vec_eq_uncurry`, `vec_bijective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`kronecker_mulVec_vec` 📖	mathematical	—	`mulVec` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `instFintypeProd` `kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `vec` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `transpose`	—	`kronecker_mulVec_vec_of_commute` `Commute.all`
`kronecker_mulVec_vec_of_commute` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`mulVec` `instFintypeProd` `kroneckerMap` `vec` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `transpose`	—	`Finset.sum_congr` `Finset.sum_mul` `Finset.sum_product` `Commute.right_comm` `Commute.eq`
`star_vec` 📖	mathematical	—	`Star.star` `Pi.instStarForall` `vec` `map`	—	—
`star_vec_dotProduct_vec` 📖	mathematical	—	`dotProduct` `instFintypeProd` `Star.star` `Pi.instStarForall` `vec` `trace` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `conjTranspose`	—	`vec_dotProduct_vec` `transpose_transpose`
`vec_add` 📖	mathematical	—	`vec` `Matrix` `add` `Pi.instAdd`	—	—
`vec_bijective` 📖	mathematical	—	`Function.Bijective` `Matrix` `vec`	—	`Function.Bijective.comp` `Equiv.bijective` `Function.swap_bijective`
`vec_dotProduct_vec` 📖	mathematical	—	`dotProduct` `instFintypeProd` `vec` `trace` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `transpose`	—	`Finset.sum_congr` `Finset.sum_product`
`vec_eq_uncurry` 📖	mathematical	—	`vec`	—	—
`vec_eq_zero_iff` 📖	mathematical	—	`vec` `Pi.instZero` `Matrix` `zero`	—	—
`vec_hadamard` 📖	mathematical	—	`vec` `hadamard` `Pi.instMul`	—	—
`vec_inj` 📖	mathematical	—	`vec`	—	—
`vec_map` 📖	mathematical	—	`vec` `map`	—	—
`vec_mul_eq_mulVec` 📖	mathematical	—	`vec` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `mulVec` `instFintypeProd` `kroneckerMap` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`kronecker_mulVec_vec_of_commute` `eq_or_ne` `one_apply_eq` `one_apply_ne` `transpose_one` `mul_one`
`vec_mul_eq_vecMul` 📖	mathematical	—	`vec` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `vecMul` `instFintypeProd` `kroneckerMap` `one` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`vec_vecMul_kronecker_of_commute` `eq_or_ne` `one_apply_eq` `one_apply_ne` `transpose_one` `one_mul`
`vec_neg` 📖	mathematical	—	`vec` `Matrix` `neg` `Pi.instNeg`	—	—
`vec_of` 📖	mathematical	—	`vec` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of`	—	—
`vec_single` 📖	mathematical	—	`vec` `single` `Pi.single`	—	`single_eq_of_single_single` `vec_of` `Function.uncurry_flip` `Pi.uncurry_single_single` `Pi.single_comp_equiv`
`vec_smul` 📖	mathematical	—	`vec` `Matrix` `smul` `Function.hasSMul`	—	—
`vec_sub` 📖	mathematical	—	`vec` `Matrix` `sub` `Pi.instSub`	—	—
`vec_sum` 📖	mathematical	—	`vec` `Finset.sum` `Matrix` `addCommMonoid` `Pi.addCommMonoid`	—	`Finset.sum_apply` `Finset.sum_congr` `sum_apply`
`vec_transpose` 📖	mathematical	—	`vec` `transpose`	—	—
`vec_vecMul_kronecker` 📖	mathematical	—	`vecMul` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `NonUnitalCommSemiring.toNonUnitalSemiring` `instFintypeProd` `vec` `kroneckerMap` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `transpose`	—	`vec_vecMul_kronecker_of_commute` `Commute.all`
`vec_vecMul_kronecker_of_commute` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	`vecMul` `instFintypeProd` `vec` `kroneckerMap` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `transpose`	—	`Finset.sum_congr` `Finset.sum_mul` `Finset.sum_product` `Commute.eq` `Commute.right_comm` `mul_assoc`
`vec_zero` 📖	mathematical	—	`vec` `Matrix` `zero` `Pi.instZero`	—	—

Nat.Partrec'

Definitions

Name	Category	Theorems
`Vec` 📖	MathDef	4 math math: `idv`, `nil`, `Vec.prim`, `vec_iff`

Nat.Primrec'

Definitions

Name	Category	Theorems
`Vec` 📖	MathDef	3 math math: `idv`, `nil`, `vec_iff`

---

← Back to Index