Documentation Verification Report

KroneckerDelta

📁 Source: PhysLean/Mathematics/KroneckerDelta.lean

Statistics

Metric	Count
Definitions `kroneckerDelta`, `«termδ[_,_]»`	2
Theorems `eq_of_coe`, `eq_one_of_same`, `eq_zero_of_ne`, `eq_zero_of_not`, `finset_sum_smul`, `finset_sum_sum_smul_eq_zero`, `smul_eq_zero_iff`, `smul_eq_zero_iff'`, `smul_eq_zero_iff''`, `smul_of_eq_zero`, `smul_sub_eq_zero`, `smul_symm`, `sum_mul`, `sum_smul`, `sum_sum_smul_eq_zero`, `symm`, `symmetrize`, `symmetrize'`	18
Total	20

KroneckerDelta

Definitions

Name	Category	Theorems
`kroneckerDelta` 📖	CompOp	27 math math: `QuantumMechanics.HydrogenAtom.angularMomentum_commutation_lrl`, `sum_smul`, `QuantumMechanics.position_commutation_momentum_momentum`, `eq_zero_of_ne`, `smul_eq_zero_iff`, `QuantumMechanics.momentum_comp_angularMomentum_eq`, `QuantumMechanics.angularMomentum_commutation_position`, `QuantumMechanics.angularMomentum_commutation_angularMomentum`, `finset_sum_sum_smul_eq_zero`, `symmetrize'`, `QuantumMechanics.position_commutation_momentum`, `QuantumMechanics.momentum_comp_position_eq`, `smul_sub_eq_zero`, `finset_sum_smul`, `symm`, `smul_eq_zero_iff'`, `QuantumMechanics.position_position_commutation_momentum`, `smul_symm`, `sum_mul`, `eq_of_coe`, `eq_zero_of_not`, `eq_one_of_same`, `sum_sum_smul_eq_zero`, `QuantumMechanics.angularMomentum_commutation_momentum`, `symmetrize`, `smul_of_eq_zero`, `smul_eq_zero_iff''`
`«termδ[_,_]»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_coe` 📖	mathematical	—	`kroneckerDelta`	—	`eq_one_of_same` `eq_zero_of_ne`
`eq_one_of_same` 📖	mathematical	—	`kroneckerDelta`	—	—
`eq_zero_of_ne` 📖	mathematical	—	`kroneckerDelta`	—	—
`eq_zero_of_not` 📖	mathematical	—	`kroneckerDelta`	—	`eq_zero_of_ne`
`finset_sum_smul` 📖	mathematical	—	`kroneckerDelta`	—	—
`finset_sum_sum_smul_eq_zero` 📖	mathematical	—	`kroneckerDelta`	—	`finset_sum_smul`
`smul_eq_zero_iff` 📖	mathematical	—	`kroneckerDelta`	—	`eq_one_of_same` `eq_zero_of_ne`
`smul_eq_zero_iff'` 📖	mathematical	—	`kroneckerDelta`	—	`eq_one_of_same` `smul_of_eq_zero`
`smul_eq_zero_iff''` 📖	mathematical	—	`kroneckerDelta`	—	`smul_eq_zero_iff'`
`smul_of_eq_zero` 📖	mathematical	—	`kroneckerDelta`	—	`eq_zero_of_ne`
`smul_sub_eq_zero` 📖	mathematical	—	`kroneckerDelta`	—	`eq_zero_of_ne`
`smul_symm` 📖	mathematical	—	`kroneckerDelta`	—	`eq_zero_of_ne`
`sum_mul` 📖	mathematical	—	`kroneckerDelta`	—	—
`sum_smul` 📖	mathematical	—	`kroneckerDelta`	—	—
`sum_sum_smul_eq_zero` 📖	mathematical	—	`kroneckerDelta`	—	`sum_smul`
`symm` 📖	mathematical	—	`kroneckerDelta`	—	—
`symmetrize` 📖	mathematical	—	`kroneckerDelta`	—	`eq_one_of_same` `eq_zero_of_ne`
`symmetrize'` 📖	mathematical	—	`kroneckerDelta`	—	`eq_one_of_same` `eq_zero_of_ne`

---

← Back to Index