Hadamard

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

Statistics

Metric	Count
Definitions `hadamard`, `«term_⊙_»`	2
Theorems `add_hadamard`, `diagonal_hadamard`, `diagonal_hadamard_diagonal`, `diagonal_hadamard_eq_diagonal_iff`, `dotProduct_vecMul_hadamard`, `hadamard_add`, `hadamard_apply`, `hadamard_assoc`, `hadamard_comm`, `hadamard_diagonal`, `hadamard_diagonal_eq_diagonal_iff`, `hadamard_of_one`, `hadamard_one`, `hadamard_one_eq_diagonal_iff`, `hadamard_one_eq_one_iff`, `hadamard_one_eq_zero_iff`, `hadamard_self_eq_self_iff`, `hadamard_smul`, `hadamard_zero`, `of_one_hadamard`, `one_hadamard`, `one_hadamard_eq_diagonal_iff`, `one_hadamard_eq_one_iff`, `one_hadamard_eq_zero_iff`, `single_hadamard_single_eq`, `single_hadamard_single_of_ne`, `smul_hadamard`, `sum_hadamard_eq`, `zero_hadamard`	29
Total	31

Matrix

Definitions

Name	Category	Theorems
`hadamard` 📖	CompOp	31 math math: `hadamard_self_eq_self_iff`, `single_hadamard_single_eq`, `hadamard_smul`, `hadamard_one_eq_zero_iff`, `sum_hadamard_eq`, `hadamard_diagonal_eq_diagonal_iff`, `hadamard_assoc`, `hadamard_of_one`, `hadamard_one`, `vec_hadamard`, `of_one_hadamard`, `hadamard_apply`, `one_hadamard_eq_diagonal_iff`, `hadamard_one_eq_one_iff`, `one_hadamard_eq_one_iff`, `single_hadamard_single_of_ne`, `one_hadamard`, `zero_hadamard`, `hadamard_zero`, `hadamard_comm`, `add_hadamard`, `one_hadamard_eq_zero_iff`, `diagonal_hadamard`, `dotProduct_vecMul_hadamard`, `isAdjMatrix_iff_hadamard`, `diagonal_hadamard_diagonal`, `smul_hadamard`, `diagonal_hadamard_eq_diagonal_iff`, `hadamard_add`, `hadamard_diagonal`, `hadamard_one_eq_diagonal_iff`
`«term_⊙_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_hadamard` 📖	mathematical	—	`hadamard` `Distrib.toMul` `Matrix` `add` `Distrib.toAdd`	—	`ext` `right_distrib` `Distrib.rightDistribClass`
`diagonal_hadamard` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `diagonal` `MulZeroClass.toZero` `Pi.instMul` `diag`	—	`ext` `ite_mul` `MulZeroClass.zero_mul`
`diagonal_hadamard_diagonal` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `diagonal` `MulZeroClass.toZero` `Pi.instMul`	—	`diagonal_hadamard` `diag_diagonal`
`diagonal_hadamard_eq_diagonal_iff` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `diagonal` `MulZeroClass.toZero` `Pi.instMul` `diag`	—	`diagonal_hadamard`
`dotProduct_vecMul_hadamard` 📖	mathematical	—	`dotProduct` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `vecMul` `hadamard` `trace` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `transpose`	—	`sum_hadamard_eq` `Finset.sum_comm` `Finset.sum_congr` `Finset.sum_mul` `mul_assoc` `diagonal_mul` `mul_diagonal`
`hadamard_add` 📖	mathematical	—	`hadamard` `Distrib.toMul` `Matrix` `add` `Distrib.toAdd`	—	`ext` `left_distrib` `Distrib.leftDistribClass`
`hadamard_apply` 📖	mathematical	—	`hadamard`	—	—
`hadamard_assoc` 📖	mathematical	—	`hadamard` `Semigroup.toMul`	—	`ext` `mul_assoc`
`hadamard_comm` 📖	mathematical	—	`hadamard` `CommMagma.toMul`	—	`ext` `mul_comm`
`hadamard_diagonal` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `diagonal` `MulZeroClass.toZero` `Pi.instMul` `diag`	—	`ext` `mul_ite` `MulZeroClass.mul_zero`
`hadamard_diagonal_eq_diagonal_iff` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `diagonal` `MulZeroClass.toZero` `Pi.instMul` `diag`	—	`hadamard_diagonal`
`hadamard_of_one` 📖	mathematical	—	`hadamard` `MulOne.toMul` `MulOneClass.toMulOne` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `Pi.instOne` `MulOne.toOne`	—	`ext` `mul_one`
`hadamard_one` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `one` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `diagonal` `diag`	—	`hadamard_diagonal` `mul_one`
`hadamard_one_eq_diagonal_iff` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `one` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `diagonal` `diag`	—	`mul_one` `hadamard_diagonal_eq_diagonal_iff`
`hadamard_one_eq_one_iff` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `one` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `diag` `Pi.instOne`	—	`hadamard_one_eq_diagonal_iff`
`hadamard_one_eq_zero_iff` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `one` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `zero` `diag` `Pi.instZero`	—	`diagonal_zero'` `hadamard_one_eq_diagonal_iff`
`hadamard_self_eq_self_iff` 📖	mathematical	—	`hadamard` `IsIdempotentElem`	—	`ext_iff`
`hadamard_smul` 📖	mathematical	—	`hadamard` `Matrix` `smul`	—	`ext` `mul_smul_comm`
`hadamard_zero` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `Matrix` `zero` `MulZeroClass.toZero`	—	`ext` `MulZeroClass.mul_zero`
`of_one_hadamard` 📖	mathematical	—	`hadamard` `MulOne.toMul` `MulOneClass.toMulOne` `DFunLike.coe` `Equiv` `Matrix` `EquivLike.toFunLike` `Equiv.instEquivLike` `of` `Pi.instOne` `MulOne.toOne`	—	`ext` `one_mul`
`one_hadamard` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `one` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `diagonal` `diag`	—	`diagonal_hadamard` `one_mul`
`one_hadamard_eq_diagonal_iff` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `one` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `diagonal` `diag`	—	`one_mul` `diagonal_hadamard_eq_diagonal_iff`
`one_hadamard_eq_one_iff` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `one` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `diag` `Pi.instOne`	—	`one_hadamard_eq_diagonal_iff`
`one_hadamard_eq_zero_iff` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `MulZeroOneClass.toMulZeroClass` `Matrix` `one` `MulZeroClass.toZero` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `zero` `diag` `Pi.instZero`	—	`diagonal_zero'` `one_hadamard_eq_diagonal_iff`
`single_hadamard_single_eq` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `single` `MulZeroClass.toZero`	—	`ext` `apply_ite₂` `MulZeroClass.zero_mul`
`single_hadamard_single_of_ne` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `single` `MulZeroClass.toZero` `Matrix` `zero`	—	`not_and_or` `ext` `mul_ite` `ite_mul` `MulZeroClass.zero_mul` `MulZeroClass.mul_zero`
`smul_hadamard` 📖	mathematical	—	`hadamard` `Matrix` `smul`	—	`ext` `smul_mul_assoc`
`sum_hadamard_eq` 📖	mathematical	—	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Finset.univ` `hadamard` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `trace` `Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `transpose`	—	—
`zero_hadamard` 📖	mathematical	—	`hadamard` `MulZeroClass.toMul` `Matrix` `zero` `MulZeroClass.toZero`	—	`ext` `MulZeroClass.zero_mul`

---

← Back to Index