Documentation Verification Report

Circulant

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

Statistics

Metric	Count
Definitions `circulant`	1
Theorems `circulant_inj`, `circulant_injective`, `circulant_isSymm_apply`, `circulant_isSymm_iff`, `circulant_ite`, `circulant_mul`, `circulant_mul_comm`, `conjTranspose_circulant`, `transpose_circulant`, `circulant_add`, `circulant_apply`, `circulant_col_zero_eq`, `circulant_inj`, `circulant_injective`, `circulant_isSymm_apply`, `circulant_isSymm_iff`, `circulant_mul`, `circulant_mul_comm`, `circulant_neg`, `circulant_single`, `circulant_single_one`, `circulant_smul`, `circulant_sub`, `circulant_zero`, `conjTranspose_circulant`, `map_circulant`, `transpose_circulant`	27
Total	28

Matrix

Definitions

Name	Category	Theorems
`circulant` 📖	CompOp	25 math math: `circulant_neg`, `circulant_smul`, `transpose_circulant`, `circulant_sub`, `circulant_apply`, `map_circulant`, `circulant_add`, `Fin.conjTranspose_circulant`, `Fin.circulant_mul_comm`, `circulant_single_one`, `Fin.circulant_inj`, `Fin.transpose_circulant`, `circulant_inj`, `circulant_zero`, `circulant_mul`, `circulant_col_zero_eq`, `circulant_mul_comm`, `circulant_single`, `Fin.circulant_isSymm_iff`, `circulant_isSymm_iff`, `Fin.circulant_injective`, `circulant_injective`, `conjTranspose_circulant`, `Fin.circulant_mul`, `Fin.circulant_ite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circulant_add` 📖	mathematical	—	`circulant` `Pi.instAdd` `Matrix` `add`	—	`ext`
`circulant_apply` 📖	mathematical	—	`circulant`	—	—
`circulant_col_zero_eq` 📖	mathematical	—	`circulant` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	`sub_zero`
`circulant_inj` 📖	mathematical	—	`circulant` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid`	—	`circulant_injective`
`circulant_injective` 📖	mathematical	—	`Matrix` `circulant` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid`	—	`circulant_col_zero_eq`
`circulant_isSymm_apply` 📖	mathematical	`IsSymm` `circulant` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	`circulant_isSymm_iff`
`circulant_isSymm_iff` 📖	mathematical	—	`IsSymm` `circulant` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	`IsSymm.eq_1` `transpose_circulant`
`circulant_mul` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `circulant` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `mulVec`	—	`ext` `Finset.sum_congr` `Fintype.sum_equiv` `sub_sub_sub_cancel_right`
`circulant_mul_comm` 📖	mathematical	—	`Matrix` `instHMulOfFintypeOfMulOfAddCommMonoid` `CommMagma.toMul` `circulant` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`ext` `Finset.sum_congr` `Fintype.sum_equiv` `add_sub_cancel_right` `mul_comm` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.const_add_termg` `add_zero` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Abel.zero_termg`
`circulant_neg` 📖	mathematical	—	`circulant` `Pi.instNeg` `Matrix` `neg`	—	`ext`
`circulant_single` 📖	mathematical	—	`circulant` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `DFunLike.coe` `RingHom` `Matrix` `nonAssocSemiring` `RingHom.instFunLike` `scalar`	—	`ext` `Pi.single_apply`
`circulant_single_one` 📖	mathematical	—	`circulant` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `Pi.single` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Matrix` `one`	—	`ext` `Pi.single_apply`
`circulant_smul` 📖	mathematical	—	`circulant` `Function.hasSMul` `Matrix` `smul`	—	—
`circulant_sub` 📖	mathematical	—	`circulant` `Pi.instSub` `Matrix` `sub`	—	`ext`
`circulant_zero` 📖	mathematical	—	`circulant` `Pi.instZero` `Matrix` `zero`	—	`ext`
`conjTranspose_circulant` 📖	mathematical	—	`conjTranspose` `circulant` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid` `Star.star` `Pi.instStarForall` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	`ext` `neg_sub`
`map_circulant` 📖	mathematical	—	`map` `circulant`	—	`ext`
`transpose_circulant` 📖	mathematical	—	`transpose` `circulant` `SubNegMonoid.toSub` `SubtractionMonoid.toSubNegMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	`ext` `neg_sub`

Matrix.Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`circulant_inj` 📖	mathematical	—	`Matrix.circulant`	—	`circulant_injective`
`circulant_injective` 📖	mathematical	—	`Matrix` `Matrix.circulant`	—	`Matrix.circulant_injective`
`circulant_isSymm_apply` 📖	—	`Matrix.IsSymm` `Matrix.circulant`	—	—	`circulant_isSymm_iff`
`circulant_isSymm_iff` 📖	mathematical	—	`Matrix.IsSymm` `Matrix.circulant`	—	`Fin.isEmpty'` `Matrix.circulant_isSymm_iff`
`circulant_ite` 📖	mathematical	—	`Matrix.circulant` `Matrix` `Matrix.one`	—	`Matrix.subsingleton_of_empty_right` `Fin.isEmpty'` `Matrix.circulant_single_one` `Pi.single_apply`
`circulant_mul` 📖	mathematical	—	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Fin.fintype` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Matrix.circulant` `Matrix.mulVec`	—	`Matrix.subsingleton_of_empty_right` `Fin.isEmpty'` `Matrix.circulant_mul`
`circulant_mul_comm` 📖	mathematical	—	`Matrix` `Matrix.instHMulOfFintypeOfMulOfAddCommMonoid` `Fin.fintype` `CommMagma.toMul` `Matrix.circulant`	—	`Matrix.circulant_mul_comm`
`conjTranspose_circulant` 📖	mathematical	—	`Matrix.conjTranspose` `Matrix.circulant` `Star.star` `Pi.instStarForall`	—	`Matrix.subsingleton_of_empty_right` `Fin.isEmpty'` `Matrix.conjTranspose_circulant`
`transpose_circulant` 📖	mathematical	—	`Matrix.transpose` `Matrix.circulant`	—	`Matrix.subsingleton_of_empty_right` `Fin.isEmpty'` `Matrix.transpose_circulant`

---

← Back to Index