Documentation Verification Report

CliffordAlgebra

📁 Source: PhysLean/Relativity/CliffordAlgebra.lean

Statistics

Metric	Count
Definitions `γ`, `diracAlgebra`, `diracForm`, `ofCliffordAlgebra`, `γSet`, `γ0`, `γ1`, `γ2`, `γ3`, `γ5`	10
Theorems `one_fin_four`, `diracForm_apply`, `ofCliffordAlgebra_range_eq_top`, `ofCliffordAlgebra_surjective`, `ofCliffordAlgebra_ι_single`, `γSet_subset_diracAlgebra`, `γ_in_diracAlgebra`, `γ_in_γSet`, `γ_subtype_in_range`, `γ0_mul_γ0`, `γ1_mul_γ0`, `γ1_mul_γ1`, `γ2_mul_γ0`, `γ2_mul_γ1`, `γ2_mul_γ2`, `γ3_mul_γ0`, `γ3_mul_γ1`, `γ3_mul_γ2`, `γ3_mul_γ3`	19
Total	29

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_fin_four` 📖	—	—	—	—	—

spaceTime

Definitions

Name	Category	Theorems
`γ` 📖	CompOp	4 math math: `γ.γ_in_γSet`, `γ.ofCliffordAlgebra_ι_single`, `γ.γ_in_diracAlgebra`, `γ.γ_subtype_in_range`
`γ0` 📖	CompOp	4 math math: `γ1_mul_γ0`, `γ2_mul_γ0`, `γ3_mul_γ0`, `γ0_mul_γ0`
`γ1` 📖	CompOp	4 math math: `γ1_mul_γ0`, `γ3_mul_γ1`, `γ1_mul_γ1`, `γ2_mul_γ1`
`γ2` 📖	CompOp	4 math math: `γ2_mul_γ1`, `γ2_mul_γ0`, `γ3_mul_γ2`, `γ2_mul_γ2`
`γ3` 📖	CompOp	4 math math: `γ3_mul_γ1`, `γ3_mul_γ0`, `γ3_mul_γ2`, `γ3_mul_γ3`
`γ5` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`γ0_mul_γ0` 📖	mathematical	—	`γ0`	—	`Matrix.one_fin_four`
`γ1_mul_γ0` 📖	mathematical	—	`γ1` `γ0`	—	—
`γ1_mul_γ1` 📖	mathematical	—	`γ1`	—	`Matrix.one_fin_four`
`γ2_mul_γ0` 📖	mathematical	—	`γ2` `γ0`	—	—
`γ2_mul_γ1` 📖	mathematical	—	`γ2` `γ1`	—	—
`γ2_mul_γ2` 📖	mathematical	—	`γ2`	—	`Matrix.one_fin_four`
`γ3_mul_γ0` 📖	mathematical	—	`γ3` `γ0`	—	—
`γ3_mul_γ1` 📖	mathematical	—	`γ3` `γ1`	—	—
`γ3_mul_γ2` 📖	mathematical	—	`γ3` `γ2`	—	—
`γ3_mul_γ3` 📖	mathematical	—	`γ3`	—	`Matrix.one_fin_four`

spaceTime.γ

Definitions

Name	Category	Theorems
`diracAlgebra` 📖	CompOp	6 math math: `ofCliffordAlgebra_surjective`, `ofCliffordAlgebra_ι_single`, `γ_in_diracAlgebra`, `ofCliffordAlgebra_range_eq_top`, `γSet_subset_diracAlgebra`, `γ_subtype_in_range`
`diracForm` 📖	CompOp	5 math math: `ofCliffordAlgebra_surjective`, `diracForm_apply`, `ofCliffordAlgebra_ι_single`, `ofCliffordAlgebra_range_eq_top`, `γ_subtype_in_range`
`ofCliffordAlgebra` 📖	CompOp	4 math math: `ofCliffordAlgebra_surjective`, `ofCliffordAlgebra_ι_single`, `ofCliffordAlgebra_range_eq_top`, `γ_subtype_in_range`
`γSet` 📖	CompOp	2 math math: `γ_in_γSet`, `γSet_subset_diracAlgebra`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`diracForm_apply` 📖	mathematical	—	`diracForm`	—	—
`ofCliffordAlgebra_range_eq_top` 📖	mathematical	—	`diracForm` `diracAlgebra` `ofCliffordAlgebra`	—	—
`ofCliffordAlgebra_surjective` 📖	mathematical	—	`diracForm` `diracAlgebra` `ofCliffordAlgebra`	—	`ofCliffordAlgebra_range_eq_top`
`ofCliffordAlgebra_ι_single` 📖	mathematical	—	`diracForm` `diracAlgebra` `ofCliffordAlgebra` `spaceTime.γ` `γ_in_diracAlgebra`	—	`γ_in_diracAlgebra`
`γSet_subset_diracAlgebra` 📖	mathematical	—	`γSet` `diracAlgebra`	—	—
`γ_in_diracAlgebra` 📖	mathematical	—	`diracAlgebra` `spaceTime.γ`	—	`γSet_subset_diracAlgebra` `γ_in_γSet`
`γ_in_γSet` 📖	mathematical	—	`γSet` `spaceTime.γ`	—	—
`γ_subtype_in_range` 📖	mathematical	—	`diracAlgebra` `diracForm` `ofCliffordAlgebra` `spaceTime.γ` `γ_in_diracAlgebra`	—	`γ_in_diracAlgebra` `ofCliffordAlgebra_ι_single`

---

← Back to Index