Theorems · Theorem · linear algebra
Matrix.circulant_mul
∀ {α : Type u_1} {n : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n] [inst_2 : AddGroup n]
(v w : n → α), Matrix.circulant v * Matrix.circulant w = Matrix.circulant ((Matrix.circulant v).mulVec w)The product of two circulant matrices circulant v and circulant w is
the circulant matrix generated by circulant v *ᵥ w.
- Defined in
- Mathlib.LinearAlgebra.Matrix.Circulant
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 60 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fintypestatement and proof · cited by 7,736
- AddGroupstatement and proof · cited by 4,410
- Matrixstatement · cited by 4,303
- NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
- Matrix.extproof · cited by 540
- Matrix.mulVecstatement · cited by 267
- Fintype.sum_equivproof · cited by 35
- sub_sub_sub_cancel_rightproof · cited by 34
- Matrix.circulantstatement · cited by 27
- Equiv.subRightproof · cited by 10
- Equiv.subRight_applyproof · cited by 4
Cited by1
Results whose statement or proof uses this declaration.
- Matrix.Fin.circulant_mulproof · cited by 0