Documentation Verification Report

FamilyMaps

📁 Source: PhysLean/Particles/StandardModel/AnomalyCancellation/FamilyMaps.lean

Statistics

Metric	Count
Definitions `chargesMapOfSpeciesMap`, `familyEmbedding`, `familyProjection`, `familyUniversal`, `speciesEmbed`, `speciesFamilyProj`, `speciesFamilyUniversial`	7
Theorems `chargesMapOfSpeciesMap_apply`, `speciesEmbed_apply`, `speciesFamilyProj_apply`, `speciesFamilyUniversial_apply`	4
Total	11

SM

Definitions

Name	Category	Theorems
`chargesMapOfSpeciesMap` 📖	CompOp	1 math math: `chargesMapOfSpeciesMap_apply`
`familyEmbedding` 📖	CompOp	—
`familyProjection` 📖	CompOp	—
`familyUniversal` 📖	CompOp	—
`speciesEmbed` 📖	CompOp	1 math math: `speciesEmbed_apply`
`speciesFamilyProj` 📖	CompOp	1 math math: `speciesFamilyProj_apply`
`speciesFamilyUniversial` 📖	CompOp	1 math math: `speciesFamilyUniversial_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`chargesMapOfSpeciesMap_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `chargesMapOfSpeciesMap` `SMCharges.toSpeciesEquiv` `SMSpecies` `SMCharges.toSpecies`	—	—
`speciesEmbed_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `speciesEmbed`	—	—
`speciesFamilyProj_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `speciesFamilyProj`	—	—
`speciesFamilyUniversial_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `SMSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `speciesFamilyUniversial`	—	—

---

← Back to Index