Documentation Verification Report

Orthogonality

📁 Source: Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean

Statistics

Metric	Count
Definitions `instFintype`	1
Theorems `card_addChar_le`, `expect_eq_ite`, `expect_eq_zero_iff_ne_zero`, `expect_ne_zero_iff_eq_zero`, `linearIndependent`, `wInner_cWeight_eq_boole`, `wInner_cWeight_eq_one_iff_eq`, `wInner_cWeight_eq_zero_iff_ne`, `wInner_cWeight_self`	9
Total	10

AddChar

Definitions

Name	Category	Theorems
`instFintype` 📖	CompOp	8 math math: `card_addChar_le`, `AddDissociated.randomisation`, `sum_apply_eq_ite`, `expect_apply_eq_zero_iff_ne_zero`, `sum_apply_eq_zero_iff_ne_zero`, `card_eq`, `doubleDualEquiv_symm_doubleDualEmb_apply`, `expect_apply_eq_ite`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_addChar_le` 📖	mathematical	—	`Fintype.card` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `instFintype` `Finite.of_fintype`	—	`Finite.of_fintype` `Module.finrank_fintype_fun_eq_card` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `LinearIndependent.fintype_card_le_finrank` `FiniteDimensional.finiteDimensional_pi'` `Module.instFiniteDimensionalOfIsReflexive` `Module.instIsReflexiveOfFiniteOfProjective` `FiniteDimensional.finiteDimensional_self` `Module.Projective.of_free` `Module.Free.self` `linearIndependent`
`expect_eq_ite` 📖	mathematical	—	`Finset.expect` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Algebra.toModule` `NNRat` `instCommSemiringNNRat` `DivisionSemiring.toNNRatAlgebra` `Finset.univ` `DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instFunLike` `instZero` `instDecidableEq` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Fintype.expect_eq_sum_div_card` `sum_eq_ite` `ite_div` `div_self` `AddTorsor.nonempty` `zero_div`
`expect_eq_zero_iff_ne_zero` 📖	mathematical	—	`Finset.expect` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Algebra.toModule` `NNRat` `instCommSemiringNNRat` `DivisionSemiring.toNNRatAlgebra` `Finset.univ` `DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`expect_eq_ite` `Ne.ite_eq_right_iff` `one_ne_zero` `NeZero.charZero_one`
`expect_ne_zero_iff_eq_zero` 📖	mathematical	—	`AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `instZero`	—	`Iff.not_left` `expect_eq_zero_iff_ne_zero`
`linearIndependent` 📖	mathematical	—	`LinearIndependent` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `DFunLike.coe` `instFunLike` `Pi.addCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Pi.Function.module` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `RCLike.innerProductSpace`	—	`nonempty_fintype` `RCLike.linearIndependent_of_ne_zero_of_wInner_cWeight_eq_zero` `coe_ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `wInner_cWeight_eq_zero_iff_ne`
`wInner_cWeight_eq_boole` 📖	mathematical	—	`RCLike.wInner` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.innerProductSpace` `RCLike.cWeight` `DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `instFunLike` `instDecidableEq` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`wInner_cWeight_self` `mul_inv_eq_one` `RCLike.charZero_rclike` `RCLike.wInner_cWeight_eq_expect` `Finset.expect_congr` `Finite.of_fintype` `map_neg_eq_inv` `expect_eq_zero_iff_ne_zero` `instIsDomain`
`wInner_cWeight_eq_one_iff_eq` 📖	mathematical	—	`RCLike.wInner` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.innerProductSpace` `RCLike.cWeight` `DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `instFunLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`wInner_cWeight_eq_boole` `Ne.ite_eq_left_iff` `one_ne_zero` `NeZero.charZero_one` `RCLike.charZero_rclike`
`wInner_cWeight_eq_zero_iff_ne` 📖	mathematical	—	`RCLike.wInner` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.innerProductSpace` `RCLike.cWeight` `DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing`	—	`wInner_cWeight_eq_boole` `Ne.ite_eq_right_iff` `one_ne_zero` `NeZero.charZero_one` `RCLike.charZero_rclike`
`wInner_cWeight_self` 📖	mathematical	—	`RCLike.wInner` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RCLike.innerProductSpace` `RCLike.cWeight` `DFunLike.coe` `AddChar` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `instFunLike` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedCommRing.toNormedRing`	—	`RCLike.charZero_rclike` `RCLike.wInner_cWeight_eq_expect` `Finset.expect_congr` `inner_self_eq_norm_sq_to_K` `norm_apply` `NormedDivisionRing.toNormMulClass` `NormedDivisionRing.to_normOneClass` `Finite.of_fintype` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `one_pow` `Finset.expect_const` `AddTorsor.nonempty`

---

← Back to Index