Documentation Verification Report

Basic

📁 Source: PhysLean/Particles/SuperSymmetry/MSSMNu/AnomalyCancellation/Basic.lean

Statistics

Metric	Count
Definitions `MSSMACC`, `AnomalyFreeMk`, `AnomalyFreeMk'`, `AnomalyFreeMk''`, `AnomalyFreeQuadMk'`, `dot`, `accCube`, `accGrav`, `accQuad`, `accSU2`, `accSU3`, `accYY`, `cubeTriLin`, `cubeTriLinToFun`, `quadBiLin`, `MSSMCharges`, `D`, `E`, `Hd`, `Hu`, `L`, `N`, `Q`, `U`, `splitSMPlusH`, `toSMPlusH`, `toSMSpecies`, `toSpecies`, `toSpeciesMaps'`, `toSplitSMPlusH`, `MSSMSpecies`	31
Theorems `AnomalyFreeMk''_val`, `AnomalyFreeMk_val`, `dot_toFun_apply`, `quadSol`, `MSSMACC_cubicACC_apply`, `MSSMACC_linearACCs`, `MSSMACC_numberCharges`, `MSSMACC_numberLinear`, `MSSMACC_numberQuadratic`, `MSSMACC_quadraticACCs`, `accCube_ext`, `accGrav_ext`, `accQuad_ext`, `accSU2_ext`, `accSU3_ext`, `accYY_ext`, `cubeTriLinToFun_map_add₁`, `cubeTriLinToFun_map_smul₁`, `cubeTriLinToFun_swap1`, `cubeTriLinToFun_swap2`, `cubeTriLin_toFun_apply_apply`, `quadBiLin_toFun_apply`, `Hd_apply`, `Hd_toSpecies_inv`, `Hu_apply`, `Hu_toSpecies_inv`, `charges_eq_toSpecies_eq`, `splitSMPlusH_apply`, `splitSMPlusH_symm_apply`, `toSMPlusH_apply`, `toSMPlusH_symm_apply`, `toSMSpecies_apply`, `toSMSpecies_toSpecies_inv`, `toSpeciesMaps'_apply`, `toSpeciesMaps'_symm_apply`, `toSpecies_apply`, `toSpecies_symm_apply`, `toSplitSMPlusH_apply`, `toSplitSMPlusH_symm_apply`, `MSSMCharges_numberCharges`, `MSSMSpecies_numberCharges`	41
Total	72

MSSMACC

Definitions

Name	Category	Theorems
`AnomalyFreeMk` 📖	CompOp	1 math math: `AnomalyFreeMk_val`
`AnomalyFreeMk'` 📖	CompOp	—
`AnomalyFreeMk''` 📖	CompOp	1 math math: `AnomalyFreeMk''_val`
`AnomalyFreeQuadMk'` 📖	CompOp	—
`dot` 📖	CompOp	16 math math: `α₃_proj`, `AnomalyFreePerp.perpB₃`, `proj_val`, `α₁_proj`, `α₂_proj`, `dot_toFun_apply`, `AnomalyFreePerp.perpY₃`, `cube_proj_proj_B₃`, `cube_proj_proj_Y₃`, `quad_self_proj`, `Y₃_plus_B₃_plus_proj`, `quad_B₃_proj`, `cube_proj_proj_self`, `cube_proj`, `quad_Y₃_proj`, `quad_proj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`AnomalyFreeMk''_val` 📖	mathematical	`HomogeneousCubic` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousCubic.instFun` `MSSMACCs.accCube` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols`	`ACCSystem.Sols.toQuadSols` `AnomalyFreeMk''`	—	—
`AnomalyFreeMk_val` 📖	mathematical	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMACCs.accGrav` `MSSMACCs.accSU2` `MSSMACCs.accSU3` `MSSMACCs.accYY` `HomogeneousQuadratic` `HomogeneousQuadratic.instFun` `MSSMACCs.accQuad` `HomogeneousCubic` `HomogeneousCubic.instFun` `MSSMACCs.accCube`	`ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols` `ACCSystem.Sols.toQuadSols` `AnomalyFreeMk`	—	—
`dot_toFun_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `dot`	—	—
`quadSol` 📖	mathematical	—	`HomogeneousQuadratic` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `HomogeneousQuadratic.instFun` `MSSMACCs.accQuad` `ACCSystemLinear.LinSols.val` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemQuad.QuadSols.toLinSols`	—	`ACCSystemQuad.QuadSols.quadSol`

MSSMACCs

Definitions

Name	Category	Theorems
`accCube` 📖	CompOp	7 math math: `accCube_ext`, `MSSM.accCube_invariant`, `MSSMACC.planeY₃B₃_cubic`, `MSSMACC.lineQuad_cube`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_cube`, `MSSMACC.lineY₃B₃Charges_cubic`, `MSSMACC.lineCube_cube`
`accGrav` 📖	CompOp	2 math math: `accGrav_ext`, `MSSM.accGrav_invariant`
`accQuad` 📖	CompOp	7 math math: `MSSM.accQuad_invariant`, `MSSMACC.lineQuadAFL_quad`, `MSSMACC.planeY₃B₃_quad`, `MSSMACC.lineCube_quad`, `MSSMACC.quadSol`, `accQuad_ext`, `MSSMACC.lineY₃B₃Charges_quad`
`accSU2` 📖	CompOp	2 math math: `MSSM.accSU2_invariant`, `accSU2_ext`
`accSU3` 📖	CompOp	2 math math: `MSSM.accSU3_invariant`, `accSU3_ext`
`accYY` 📖	CompOp	2 math math: `accYY_ext`, `MSSM.accYY_invariant`
`cubeTriLin` 📖	CompOp	12 math math: `MSSMACC.α₃_proj`, `MSSMACC.doublePoint_Y₃_B₃`, `MSSMACC.planeY₃B₃_cubic`, `MSSMACC.lineY₃B₃_doublePoint`, `MSSMACC.cube_proj_proj_B₃`, `MSSMACC.cube_proj_proj_Y₃`, `MSSMACC.lineCube_quad`, `MSSMACC.doublePoint_Y₃_Y₃`, `MSSMACC.cube_proj_proj_self`, `MSSMACC.cube_proj`, `MSSMACC.doublePoint_B₃_B₃`, `cubeTriLin_toFun_apply_apply`
`cubeTriLinToFun` 📖	CompOp	4 math math: `cubeTriLinToFun_map_smul₁`, `cubeTriLinToFun_swap2`, `cubeTriLinToFun_swap1`, `cubeTriLinToFun_map_add₁`
`quadBiLin` 📖	CompOp	10 math math: `MSSMACC.α₃_proj`, `MSSMACC.planeY₃B₃_quad`, `MSSMACC.lineQuad_cube`, `MSSMACC_quadraticACCs`, `MSSMACC.quad_self_proj`, `quadBiLin_toFun_apply`, `MSSMACC.quad_B₃_proj`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `MSSMACC.quad_proj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`accCube_ext` 📖	mathematical	`ACCSystemCharges.numberCharges` `MSSMSpecies` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMCharges.toSMSpecies` `MSSMCharges.Hd` `MSSMCharges.Hu`	`HomogeneousCubic` `HomogeneousCubic.instFun` `accCube`	—	—
`accGrav_ext` 📖	mathematical	`ACCSystemCharges.numberCharges` `MSSMSpecies` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMCharges.toSMSpecies` `MSSMCharges.Hd` `MSSMCharges.Hu`	`accGrav`	—	—
`accQuad_ext` 📖	mathematical	`ACCSystemCharges.numberCharges` `MSSMSpecies` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMCharges.toSMSpecies` `MSSMCharges.Hd` `MSSMCharges.Hu`	`HomogeneousQuadratic` `HomogeneousQuadratic.instFun` `accQuad`	—	—
`accSU2_ext` 📖	mathematical	`ACCSystemCharges.numberCharges` `MSSMSpecies` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMCharges.toSMSpecies` `MSSMCharges.Hd` `MSSMCharges.Hu`	`accSU2`	—	—
`accSU3_ext` 📖	mathematical	`ACCSystemCharges.numberCharges` `MSSMSpecies` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMCharges.toSMSpecies`	`accSU3`	—	—
`accYY_ext` 📖	mathematical	`ACCSystemCharges.numberCharges` `MSSMSpecies` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `MSSMCharges.toSMSpecies` `MSSMCharges.Hd` `MSSMCharges.Hu`	`accYY`	—	—
`cubeTriLinToFun_map_add₁` 📖	mathematical	—	`cubeTriLinToFun` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid`	—	—
`cubeTriLinToFun_map_smul₁` 📖	mathematical	—	`cubeTriLinToFun` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.ChargesAddCommGroup` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule`	—	—
`cubeTriLinToFun_swap1` 📖	mathematical	—	`cubeTriLinToFun` `ACCSystemCharges.Charges` `MSSMCharges`	—	—
`cubeTriLinToFun_swap2` 📖	mathematical	—	`cubeTriLinToFun` `ACCSystemCharges.Charges` `MSSMCharges`	—	—
`cubeTriLin_toFun_apply_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `TriLinearSymm` `TriLinearSymm.instFun` `cubeTriLin`	—	—
`quadBiLin_toFun_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm` `BiLinearSymm.instFun` `quadBiLin`	—	—

MSSMCharges

Definitions

Name	Category	Theorems
`D` 📖	CompOp	—
`E` 📖	CompOp	—
`Hd` 📖	CompOp	4 math math: `Hd_toSpecies_inv`, `Hd_apply`, `charges_eq_toSpecies_eq`, `MSSM.Hd_invariant`
`Hu` 📖	CompOp	4 math math: `Hu_apply`, `MSSM.Hu_invariant`, `Hu_toSpecies_inv`, `charges_eq_toSpecies_eq`
`L` 📖	CompOp	—
`N` 📖	CompOp	—
`Q` 📖	CompOp	—
`U` 📖	CompOp	—
`splitSMPlusH` 📖	CompOp	5 math math: `splitSMPlusH_apply`, `splitSMPlusH_symm_apply`, `toSplitSMPlusH_symm_apply`, `MSSM.chargeMap_apply`, `toSpecies_symm_apply`
`toSMPlusH` 📖	CompOp	7 math math: `toSpecies_apply`, `toSMPlusH_apply`, `toSplitSMPlusH_apply`, `toSplitSMPlusH_symm_apply`, `MSSM.chargeMap_apply`, `toSpecies_symm_apply`, `toSMPlusH_symm_apply`
`toSMSpecies` 📖	CompOp	7 math math: `toSMSpecies_toSpecies_inv`, `toSMSpecies_apply`, `MSSM.repCharges_toSMSpecies`, `MSSM.chargeMap_apply`, `MSSM.toSpecies_sum_invariant`, `charges_eq_toSpecies_eq`, `MSSM.chargeMap_toSpecies`
`toSpecies` 📖	CompOp	5 math math: `toSMSpecies_toSpecies_inv`, `toSpecies_apply`, `Hd_toSpecies_inv`, `Hu_toSpecies_inv`, `toSpecies_symm_apply`
`toSpeciesMaps'` 📖	CompOp	5 math math: `toSpecies_apply`, `toSpeciesMaps'_symm_apply`, `MSSM.chargeMap_apply`, `toSpeciesMaps'_apply`, `toSpecies_symm_apply`
`toSplitSMPlusH` 📖	CompOp	2 math math: `toSplitSMPlusH_apply`, `toSplitSMPlusH_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`Hd_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `Hd`	—	—
`Hd_toSpecies_inv` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `Hd` `toSpecies`	—	—
`Hu_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `Hu`	—	—
`Hu_toSpecies_inv` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `Hu` `toSpecies`	—	—
`charges_eq_toSpecies_eq` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `MSSMSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `toSMSpecies` `Hd` `Hu`	—	—
`splitSMPlusH_apply` 📖	mathematical	—	`splitSMPlusH`	—	—
`splitSMPlusH_symm_apply` 📖	mathematical	—	`splitSMPlusH`	—	—
`toSMPlusH_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `toSMPlusH`	—	—
`toSMPlusH_symm_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `toSMPlusH`	—	—
`toSMSpecies_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `MSSMSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `toSMSpecies`	—	—
`toSMSpecies_toSpecies_inv` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `MSSMSpecies` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `toSMSpecies` `toSpecies`	—	—
`toSpeciesMaps'_apply` 📖	mathematical	—	`toSpeciesMaps'`	—	—
`toSpeciesMaps'_symm_apply` 📖	mathematical	—	`toSpeciesMaps'`	—	—
`toSpecies_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `toSpecies` `toSpeciesMaps'` `toSMPlusH`	—	—
`toSpecies_symm_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `toSpecies` `toSMPlusH` `splitSMPlusH` `toSpeciesMaps'`	—	—
`toSplitSMPlusH_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `toSplitSMPlusH` `toSMPlusH`	—	—
`toSplitSMPlusH_symm_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `toSplitSMPlusH` `toSMPlusH` `splitSMPlusH`	—	—

(root)

Definitions

Name	Category	Theorems
`MSSMACC` 📖	CompOp	59 math math: `MSSMACC.α₃_proj`, `MSSMACC.AnomalyFreePerp.toSol_inQuadCube`, `MSSMACC.AnomalyFreePerp.inQuadCubeToSol_proj`, `MSSMACC.AnomalyFreePerp.inLineEqTo_smul`, `MSSMACC.AnomalyFreePerp.perpB₃`, `MSSMACC.lineCube_smul`, `MSSMACC.AnomalyFreePerp.inQuadSolProp_iff_proj_inQuadProp`, `MSSMACC_cubicACC_apply`, `MSSMACC.proj_val`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_eq_planeY₃B₃_on_α`, `MSSMACC_numberQuadratic`, `MSSMACC.AnomalyFreePerp.toSol_surjective`, `MSSMACC_numberLinear`, `MSSMACC.planeY₃B₃_val`, `MSSMACC.α₁_proj`, `MSSMACC.AnomalyFreePerp.toSolNS_proj`, `MSSMACC.AnomalyFreePerp.inQuadToSol_proj`, `MSSMACC.doublePoint_Y₃_B₃`, `MSSMACC.α₂_proj`, `MSSMACC.AnomalyFreePerp.linEqPropSol_iff_proj_linEqProp`, `MSSMACC.B₃_val`, `MSSMACC.AnomalyFreePerp.toSol_inLineEq`, `MSSMACC.planeY₃B₃_cubic`, `MSSMACC.lineY₃B₃_doublePoint`, `MSSMACC.AnomalyFreeMk_val`, `MSSMACC.AnomalyFreePerp.perpY₃`, `MSSMACC.planeY₃B₃_smul`, `MSSMACC.Y₃_val`, `MSSMACC.lineQuadAFL_quad`, `MSSMACC.planeY₃B₃_quad`, `MSSMACC.lineQuad_cube`, `MSSMACC.cube_proj_proj_B₃`, `MSSMACC.lineQuad_smul`, `MSSMACC.cube_proj_proj_Y₃`, `MSSMACC.lineCube_quad`, `MSSMACC_linearACCs`, `MSSMACC.doublePoint_Y₃_Y₃`, `MSSMACC.AnomalyFreePerp.inLineEqToSol_proj`, `MSSMACC.quadSol`, `MSSMACC.AnomalyFreePerp.inQuadCubeToSol_smul`, `MSSMACC.AnomalyFreePerp.inQuadToSol_smul`, `MSSMACC_quadraticACCs`, `MSSMACC.quad_self_proj`, `MSSMACC.AnomalyFreePerp.toSol_inQuad`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_cube`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `MSSMACC.AnomalyFreePerp.toSol_toSolNSProj`, `MSSMACC.lineY₃B₃Charges_cubic`, `MSSMACC.lineY₃B₃Charges_quad`, `MSSMACC.AnomalyFreePerp.inCubeSolProp_iff_proj_inCubeProp`, `MSSMACC.quad_B₃_proj`, `MSSMACC_numberCharges`, `MSSMACC.cube_proj_proj_self`, `MSSMACC.cube_proj`, `MSSMACC.doublePoint_B₃_B₃`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `MSSMACC.quad_proj`, `MSSMACC.lineCube_cube`
`MSSMCharges` 📖	CompOp	66 math math: `MSSMACC.α₃_proj`, `MSSMCharges.toSMSpecies_toSpecies_inv`, `MSSM.accSU2_invariant`, `MSSMCharges.Hu_apply`, `MSSMCharges.toSpecies_apply`, `MSSMACC.AnomalyFreePerp.perpB₃`, `MSSMCharges.toSMPlusH_apply`, `MSSM.accSU3_invariant`, `MSSM.accCube_invariant`, `MSSM.Hu_invariant`, `MSSM.accQuad_invariant`, `MSSMACC_cubicACC_apply`, `MSSMACCs.cubeTriLinToFun_map_smul₁`, `MSSMACC.proj_val`, `MSSMACC.α₁_proj`, `MSSMCharges.Hd_toSpecies_inv`, `MSSMACC.doublePoint_Y₃_B₃`, `MSSMACC.α₂_proj`, `MSSMACCs.cubeTriLinToFun_swap2`, `MSSMCharges.toSplitSMPlusH_apply`, `MSSMACC.planeY₃B₃_cubic`, `MSSMACC.lineY₃B₃_doublePoint`, `MSSMCharges.toSplitSMPlusH_symm_apply`, `MSSM.accGrav_invariant`, `MSSMACC.dot_toFun_apply`, `MSSMCharges.Hd_apply`, `MSSMACC.AnomalyFreePerp.perpY₃`, `MSSMCharges.toSMSpecies_apply`, `MSSMACC.lineQuadAFL_quad`, `MSSMACC.planeY₃B₃_quad`, `MSSMACC.lineQuad_cube`, `MSSMACC.cube_proj_proj_B₃`, `MSSMACC.cube_proj_proj_Y₃`, `MSSMACC.lineCube_quad`, `MSSMACCs.cubeTriLinToFun_swap1`, `MSSM.repCharges_toSMSpecies`, `MSSMACC_linearACCs`, `MSSMCharges.Hu_toSpecies_inv`, `MSSM.chargeMap_apply`, `MSSMACC.doublePoint_Y₃_Y₃`, `MSSMACC.quadSol`, `MSSMCharges.toSpecies_symm_apply`, `MSSMACC_quadraticACCs`, `MSSMACC.quad_self_proj`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_cube`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `MSSM.toSpecies_sum_invariant`, `MSSMACC.lineY₃B₃Charges_cubic`, `MSSMACC.lineY₃B₃Charges_quad`, `MSSMACCs.quadBiLin_toFun_apply`, `MSSMACC.quad_B₃_proj`, `MSSMCharges_numberCharges`, `MSSMACC.cube_proj_proj_self`, `MSSMCharges.charges_eq_toSpecies_eq`, `MSSMACC.cube_proj`, `MSSMACC.doublePoint_B₃_B₃`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `MSSM.accYY_invariant`, `MSSMACCs.cubeTriLin_toFun_apply_apply`, `MSSMACCs.cubeTriLinToFun_map_add₁`, `MSSM.Hd_invariant`, `MSSMACC.quad_proj`, `MSSMCharges.toSMPlusH_symm_apply`, `MSSM.chargeMap_toSpecies`, `MSSMACC.lineCube_cube`
`MSSMSpecies` 📖	CompOp	8 math math: `MSSMCharges.toSMSpecies_toSpecies_inv`, `MSSMSpecies_numberCharges`, `MSSMCharges.toSMSpecies_apply`, `MSSM.repCharges_toSMSpecies`, `MSSM.chargeMap_apply`, `MSSM.toSpecies_sum_invariant`, `MSSMCharges.charges_eq_toSpecies_eq`, `MSSM.chargeMap_toSpecies`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`MSSMACC_cubicACC_apply` 📖	mathematical	—	`ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `ACCSystem.cubicACC` `MSSMACC`	—	—
`MSSMACC_linearACCs` 📖	mathematical	—	`ACCSystemLinear.linearACCs` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule`	—	—
`MSSMACC_numberCharges` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `ACCSystemLinear.toACCSystemCharges` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC`	—	—
`MSSMACC_numberLinear` 📖	mathematical	—	`ACCSystemLinear.numberLinear` `ACCSystemQuad.toACCSystemLinear` `ACCSystem.toACCSystemQuad` `MSSMACC`	—	—
`MSSMACC_numberQuadratic` 📖	mathematical	—	`ACCSystemQuad.numberQuadratic` `ACCSystem.toACCSystemQuad` `MSSMACC`	—	—
`MSSMACC_quadraticACCs` 📖	mathematical	—	`ACCSystemQuad.quadraticACCs` `ACCSystem.toACCSystemQuad` `MSSMACC` `ACCSystemCharges.Charges` `MSSMCharges` `ACCSystemCharges.chargesAddCommMonoid` `ACCSystemCharges.chargesModule` `BiLinearSymm.toHomogeneousQuad` `MSSMACCs.quadBiLin`	—	—
`MSSMCharges_numberCharges` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `MSSMCharges`	—	—
`MSSMSpecies_numberCharges` 📖	mathematical	—	`ACCSystemCharges.numberCharges` `MSSMSpecies`	—	—

---

← Back to Index