Documentation Verification Report

ZMod

📁 Source: PhysLean/Particles/SuperSymmetry/SU5/ChargeSpectrum/ZMod.lean

Statistics

Metric	Count
Definitions `ZModCharges`, `ZModZModCharges`	2
Theorems `ZModCharges_five_eq`, `ZModCharges_four_eq`, `ZModCharges_one_eq`, `ZModCharges_six_eq`, `ZModCharges_three_eq`, `ZModCharges_two_eq`	6
Total	8

SuperSymmetry.SU5.ChargeSpectrum

Definitions

Name	Category	Theorems
`ZModCharges` 📖	CompOp	6 math math: `ZModCharges_three_eq`, `ZModCharges_six_eq`, `ZModCharges_one_eq`, `ZModCharges_five_eq`, `ZModCharges_two_eq`, `ZModCharges_four_eq`
`ZModZModCharges` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ZModCharges_five_eq` 📖	mathematical	—	`ZModCharges` `SuperSymmetry.SU5.ChargeSpectrum`	—	—
`ZModCharges_four_eq` 📖	mathematical	—	`ZModCharges` `SuperSymmetry.SU5.ChargeSpectrum` `instDecidableEq`	—	—
`ZModCharges_one_eq` 📖	mathematical	—	`ZModCharges` `SuperSymmetry.SU5.ChargeSpectrum`	—	—
`ZModCharges_six_eq` 📖	mathematical	—	`ZModCharges` `SuperSymmetry.SU5.ChargeSpectrum` `instDecidableEq`	—	—
`ZModCharges_three_eq` 📖	mathematical	—	`ZModCharges` `SuperSymmetry.SU5.ChargeSpectrum`	—	—
`ZModCharges_two_eq` 📖	mathematical	—	`ZModCharges` `SuperSymmetry.SU5.ChargeSpectrum`	—	—

---

← Back to Index