Basic

📁 Source: PhysLean/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/Basic.lean

Statistics

Metric	Count
Definitions accCube, accGrav, accQuad, accSU2, accSU3, accYY, cubeTriLin, quadBiLin, SMνCharges, D, E, L, N, Q, U, toSpecies, toSpeciesEquiv, SMνSpecies	18
Theorems accCube_decomp, accCube_ext, accGrav_decomp, accGrav_ext, accQuad_decomp, accQuad_ext, accSU2_decomp, accSU2_ext, accSU3_decomp, accSU3_ext, accYY_decomp, accYY_ext, cubeTriLin_decomp, cubeTriLin_toFun_apply_apply, quadBiLin_decomp, quadBiLin_toFun_apply, charges_eq_toSpecies_eq, toSMSpecies_toSpecies_inv, toSpeciesEquiv_apply, toSpeciesEquiv_symm_apply, toSpecies_apply, toSpecies_one, SMνCharges_numberCharges, SMνSpecies_numberCharges	24
Total	42

SMνACCs

Definitions

Name	Category	Theorems
accCube 📖	CompOp	14 math math: SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube, accCube_decomp, SMRHN.SM.cubeSol, accCube_ext, SMRHN.SM.PlaneSeven.B_in_accCube, SMRHN.PlusU1.Y.add_AF_cube, SMRHN.familyUniversal_accCube, SMRHN.PlusU1.BL.add_AFL_cube, SMRHN.PlusU1.Y.add_AFL_cube, SMRHN.PlusU1.QuadSolToSol.cube_α₁_α₂_zero, SMRHN.PlusU1.cubeSol, SMRHN.SMNoGrav.cubeSol, SMRHN.PlusU1.Y.add_AFQ_cube, SMRHN.accCube_invariant
accGrav 📖	CompOp	7 math math: SMRHN.PlusU1.BL.on_cubeTriLin, SMRHN.accGrav_invariant, SMRHN.SM.gravSol, SMRHN.PlusU1.gravSol, accGrav_ext, SMRHN.familyUniversal_accGrav, accGrav_decomp
accQuad 📖	CompOp	14 math math: SMRHN.PlusU1.ElevenPlane.on_accQuad, SMRHN.PlusU1.BL.add_quad, accQuad_decomp, SMRHN.PlusU1.Y.on_cubeTriLin', accQuad_ext, SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero, SMRHN.PlusU1.Y.add_AFL_quad, SMRHN.accQuad_invariant, SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂, SMRHN.PlusU1.BL.add_AFL_quad, SMRHN.PlusU1.QuadSol.add_AFL_quad, SMRHN.familyUniversal_accQuad, SMRHN.PlusU1.Y.add_quad, SMRHN.PlusU1.quadSol
accSU2 📖	CompOp	8 math math: SMRHN.accSU2_invariant, SMRHN.familyUniversal_accSU2, SMRHN.SMNoGrav.SU2Sol, SMRHN.SM.SU2Sol, SMRHN.PlusU1.SU2Sol, accSU2_decomp, SMRHN.PlusU1.BL.on_quadBiLin, accSU2_ext
accSU3 📖	CompOp	9 math math: SMRHN.accSU3_invariant, SMRHN.PlusU1.BL.on_cubeTriLin, accSU3_decomp, accSU3_ext, SMRHN.SM.SU3Sol, SMRHN.SMNoGrav.SU3Sol, SMRHN.PlusU1.BL.on_quadBiLin, SMRHN.familyUniversal_accSU3, SMRHN.PlusU1.SU3Sol
accYY 📖	CompOp	8 math math: SMRHN.PlusU1.Y.on_quadBiLin, SMRHN.PlusU1.Y.on_cubeTriLin, SMRHN.PlusU1.YYsol, accYY_ext, SMRHN.PlusU1.BL.on_quadBiLin, SMRHN.accYY_invariant, SMRHN.familyUniversal_accYY, accYY_decomp
cubeTriLin 📖	CompOp	29 math math: SMRHN.SM.PlaneSeven.Bi_Bj_ne_cubic, SMRHN.SM.PlaneSeven.B₄_Bi_cubic, SMRHN.PlusU1.BL.on_cubeTriLin, SMRHN.SM.PlaneSeven.B₅_Bi_cubic, SMRHN.SM.PlaneSeven.Bi_Bi_Bj_cubic, SMRHN.SM.PlaneSeven.B₃_cubic, cubeTriLin_decomp, SMRHN.SM.PlaneSeven.Bi_Bj_Bk_cubic, SMRHN.SM.PlaneSeven.B₆_Bi_cubic, SMRHN.PlusU1.Y.on_cubeTriLin, SMRHN.SM.PlaneSeven.B₅_cubic, SMRHN.PlusU1.Y.on_cubeTriLin', SMRHN.SM.PlaneSeven.B₃_Bi_cubic, SMRHN.SM.PlaneSeven.B₆_cubic, SMRHN.PlusU1.BL.add_AFL_cube, SMRHN.SM.PlaneSeven.B₀_cubic, SMRHN.SM.PlaneSeven.B₁_Bi_cubic, SMRHN.PlusU1.Y.add_AFL_cube, SMRHN.SM.PlaneSeven.B₀_Bi_cubic, SMRHN.SM.PlaneSeven.B₂_cubic, SMRHN.PlusU1.Y.on_cubeTriLin'_ALQ, SMRHN.SM.PlaneSeven.B₂_Bi_cubic, SMRHN.SM.PlaneSeven.B₄_cubic, cubeTriLin_toFun_apply_apply, SMRHN.SM.PlaneSeven.B₁_cubic, SMRHN.PlusU1.Y.on_cubeTriLin_AFL, SMRHN.familyUniversal_cubeTriLin', SMRHN.PlusU1.BL.on_cubeTriLin_AFL, SMRHN.familyUniversal_cubeTriLin
quadBiLin 📖	CompOp	12 math math: SMRHN.familyUniversal_quadBiLin, SMRHN.PlusU1.ElevenPlane.Bi_Bj_quad, SMRHN.PlusU1.Y.on_quadBiLin_AFL, quadBiLin_decomp, SMRHN.PlusU1.Y.on_quadBiLin, SMRHN.PlusU1.BL.on_quadBiLin_AFL, quadBiLin_toFun_apply, SMRHN.PlusU1.ElevenPlane.Bi_sum_quad, SMRHN.PlusU1_quadraticACCs, SMRHN.PlusU1.ElevenPlane.quadCoeff_eq_bilinear, SMRHN.PlusU1.QuadSol.add_AFL_quad, SMRHN.PlusU1.BL.on_quadBiLin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
accCube_decomp 📖	mathematical	—	HomogeneousCubic ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousCubic.instFun accCube ACCSystemCharges.numberCharges SMνSpecies SMνCharges.Q SMνCharges.U SMνCharges.D SMνCharges.L SMνCharges.E SMνCharges.N	—	cubeTriLin_decomp
accCube_ext 📖	mathematical	ACCSystemCharges.numberCharges SMνSpecies ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule SMνCharges.toSpecies	HomogeneousCubic HomogeneousCubic.instFun accCube	—	accCube_decomp
accGrav_decomp 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule accGrav ACCSystemCharges.numberCharges SMνSpecies SMνCharges.Q SMνCharges.U SMνCharges.D SMνCharges.L SMνCharges.E SMνCharges.N	—	—
accGrav_ext 📖	mathematical	ACCSystemCharges.numberCharges SMνSpecies ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule SMνCharges.toSpecies	accGrav	—	accGrav_decomp
accQuad_decomp 📖	mathematical	—	HomogeneousQuadratic ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule HomogeneousQuadratic.instFun accQuad ACCSystemCharges.numberCharges SMνSpecies SMνCharges.Q SMνCharges.U SMνCharges.D SMνCharges.L SMνCharges.E	—	quadBiLin_decomp
accQuad_ext 📖	mathematical	ACCSystemCharges.numberCharges SMνSpecies ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule SMνCharges.toSpecies	HomogeneousQuadratic HomogeneousQuadratic.instFun accQuad	—	accQuad_decomp
accSU2_decomp 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule accSU2 ACCSystemCharges.numberCharges SMνSpecies SMνCharges.Q SMνCharges.L	—	—
accSU2_ext 📖	mathematical	ACCSystemCharges.numberCharges SMνSpecies ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule SMνCharges.toSpecies	accSU2	—	accSU2_decomp
accSU3_decomp 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule accSU3 ACCSystemCharges.numberCharges SMνSpecies SMνCharges.Q SMνCharges.U SMνCharges.D	—	—
accSU3_ext 📖	mathematical	ACCSystemCharges.numberCharges SMνSpecies ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule SMνCharges.toSpecies	accSU3	—	accSU3_decomp
accYY_decomp 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule accYY ACCSystemCharges.numberCharges SMνSpecies SMνCharges.Q SMνCharges.U SMνCharges.D SMνCharges.L SMνCharges.E	—	—
accYY_ext 📖	mathematical	ACCSystemCharges.numberCharges SMνSpecies ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule SMνCharges.toSpecies	accYY	—	accYY_decomp
cubeTriLin_decomp 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule TriLinearSymm TriLinearSymm.instFun cubeTriLin ACCSystemCharges.numberCharges SMνSpecies SMνCharges.Q SMνCharges.U SMνCharges.D SMνCharges.L SMνCharges.E SMνCharges.N	—	cubeTriLin.eq_1
cubeTriLin_toFun_apply_apply 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule TriLinearSymm TriLinearSymm.instFun cubeTriLin	—	—
quadBiLin_decomp 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule BiLinearSymm BiLinearSymm.instFun quadBiLin ACCSystemCharges.numberCharges SMνSpecies SMνCharges.Q SMνCharges.U SMνCharges.D SMνCharges.L SMνCharges.E	—	quadBiLin.eq_1
quadBiLin_toFun_apply 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule BiLinearSymm BiLinearSymm.instFun quadBiLin	—	—

SMνCharges

Definitions

Name	Category	Theorems
D 📖	CompOp	10 math math: SMRHN.familyUniversal_quadBiLin, SMνACCs.accCube_decomp, SMνACCs.quadBiLin_decomp, SMνACCs.accSU3_decomp, SMνACCs.cubeTriLin_decomp, SMνACCs.accQuad_decomp, SMνACCs.accGrav_decomp, SMRHN.familyUniversal_cubeTriLin', SMRHN.familyUniversal_cubeTriLin, SMνACCs.accYY_decomp
E 📖	CompOp	9 math math: SMRHN.familyUniversal_quadBiLin, SMνACCs.accCube_decomp, SMνACCs.quadBiLin_decomp, SMνACCs.cubeTriLin_decomp, SMνACCs.accQuad_decomp, SMνACCs.accGrav_decomp, SMRHN.familyUniversal_cubeTriLin', SMRHN.familyUniversal_cubeTriLin, SMνACCs.accYY_decomp
L 📖	CompOp	10 math math: SMRHN.familyUniversal_quadBiLin, SMνACCs.accCube_decomp, SMνACCs.quadBiLin_decomp, SMνACCs.cubeTriLin_decomp, SMνACCs.accQuad_decomp, SMνACCs.accSU2_decomp, SMνACCs.accGrav_decomp, SMRHN.familyUniversal_cubeTriLin', SMRHN.familyUniversal_cubeTriLin, SMνACCs.accYY_decomp
N 📖	CompOp	5 math math: SMνACCs.accCube_decomp, SMνACCs.cubeTriLin_decomp, SMνACCs.accGrav_decomp, SMRHN.familyUniversal_cubeTriLin', SMRHN.familyUniversal_cubeTriLin
Q 📖	CompOp	11 math math: SMRHN.familyUniversal_quadBiLin, SMνACCs.accCube_decomp, SMνACCs.quadBiLin_decomp, SMνACCs.accSU3_decomp, SMνACCs.cubeTriLin_decomp, SMνACCs.accQuad_decomp, SMνACCs.accSU2_decomp, SMνACCs.accGrav_decomp, SMRHN.familyUniversal_cubeTriLin', SMRHN.familyUniversal_cubeTriLin, SMνACCs.accYY_decomp
U 📖	CompOp	10 math math: SMRHN.familyUniversal_quadBiLin, SMνACCs.accCube_decomp, SMνACCs.quadBiLin_decomp, SMνACCs.accSU3_decomp, SMνACCs.cubeTriLin_decomp, SMνACCs.accQuad_decomp, SMνACCs.accGrav_decomp, SMRHN.familyUniversal_cubeTriLin', SMRHN.familyUniversal_cubeTriLin, SMνACCs.accYY_decomp
toSpecies 📖	CompOp	14 math math: SMRHN.sum_familyUniversal_one, SMRHN.toSpecies_familyUniversal, SMRHN.sum_familyUniversal_three, SMRHN.repCharges_toSpecies, toSMSpecies_toSpecies_inv, toSpecies_one, SMRHN.chargesMapOfSpeciesMap_toSpecies, SMRHN.toSpecies_sum_invariant, charges_eq_toSpecies_eq, SMRHN.chargeMap_apply, SMRHN.chargesMapOfSpeciesMap_apply, SMRHN.sum_familyUniversal, SMRHN.sum_familyUniversal_two, toSpecies_apply
toSpeciesEquiv 📖	CompOp	5 math math: toSpeciesEquiv_apply, toSMSpecies_toSpecies_inv, SMRHN.chargeMap_apply, SMRHN.chargesMapOfSpeciesMap_apply, toSpeciesEquiv_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charges_eq_toSpecies_eq 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges SMνSpecies ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule toSpecies	—	—
toSMSpecies_toSpecies_inv 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges SMνSpecies ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule toSpecies toSpeciesEquiv	—	—
toSpeciesEquiv_apply 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges toSpeciesEquiv	—	—
toSpeciesEquiv_symm_apply 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges toSpeciesEquiv	—	—
toSpecies_apply 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges SMνSpecies ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule toSpecies	—	—
toSpecies_one 📖	mathematical	—	ACCSystemCharges.Charges SMνCharges SMνSpecies ACCSystemCharges.chargesAddCommMonoid ACCSystemCharges.chargesModule toSpecies ACCSystemCharges.numberCharges	—	—

(root)

Definitions

Name	Category	Theorems
SMνCharges 📖	CompOp	111 math math: SMRHN.sum_familyUniversal_one, SMRHN.SM.PlaneSeven.Bi_Bj_ne_cubic, SMRHN.accSU3_invariant, SMRHN.toSpecies_familyUniversal, SMRHN.SMNoGrav_quadraticACCs, SMRHN.sum_familyUniversal_three, SMRHN.SM.PlaneSeven.B₄_Bi_cubic, SMνCharges.toSpeciesEquiv_apply, SMRHN.familyUniversal_quadBiLin, SMRHN.PlusU1.BL.on_cubeTriLin, SMRHN.repCharges_toSpecies, SMRHN.PlusU1.ElevenPlane.Bi_Bj_quad, SMRHN.PlusU1.Y.on_quadBiLin_AFL, SMRHN.SMNoGrav_linearACCs, SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube, SMRHN.SM.PlaneSeven.B₅_Bi_cubic, SMRHN.accSU2_invariant, SMνACCs.accCube_decomp, SMRHN.familyUniversal_accSU2, SMνACCs.quadBiLin_decomp, SMRHN.SM_linearACCs, SMνACCs.accSU3_decomp, SMRHN.PlusU1_linearACCs, SMRHN.SM.cubeSol, SMνCharges.toSMSpecies_toSpecies_inv, SMRHN.accGrav_invariant, SMνCharges.toSpecies_one, SMRHN.PlusU1.ElevenPlane.on_accQuad, SMRHN.SM.PlaneSeven.Bi_Bi_Bj_cubic, SMRHN.SM.PlaneSeven.B₃_cubic, SMRHN.PlusU1.Y_val, SMνACCs.cubeTriLin_decomp, SMRHN.SM.gravSol, SMRHN.SM.PlaneSeven.Bi_Bj_Bk_cubic, SMRHN.SM.SU3Sol, SMRHN.PlusU1.BL.add_quad, SMRHN.PlusU1.Y.on_quadBiLin, SMRHN.SM.PlaneSeven.B₆_Bi_cubic, SMRHN.SM_quadraticACCs, SMRHN.PlusU1.BL.on_quadBiLin_AFL, SMRHN.SM.PlaneSeven.B_in_accCube, SMRHN.PlusU1.Y.on_cubeTriLin, SMRHN.SM.PlaneSeven.B₅_cubic, SMνACCs.accQuad_decomp, SMRHN.SMNoGrav_cubicACC_apply, SMνACCs.quadBiLin_toFun_apply, SMRHN.chargesMapOfSpeciesMap_toSpecies, SMRHN.PlusU1.Y.on_cubeTriLin', SMRHN.SMNoGrav.SU2Sol, SMRHN.PlusU1.gravSol, SMRHN.PlusU1_cubicACC_apply, SMRHN.PlusU1.Y.add_AF_cube, SMRHN.PlusU1.BL_val, SMRHN.SM.PlaneSeven.B₃_Bi_cubic, SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero, SMRHN.toSpecies_sum_invariant, SMRHN.familyUniversal_accCube, SMRHN.SM.PlaneSeven.B₆_cubic, SMνCharges.charges_eq_toSpecies_eq, SMRHN.SM.SU2Sol, SMRHN.PlusU1.Y.add_AFL_quad, SMRHN.chargeMap_apply, SMRHN.PlusU1.BL.add_AFL_cube, SMRHN.SM.PlaneSeven.B₀_cubic, SMRHN.SM.PlaneSeven.B₁_Bi_cubic, SMRHN.accQuad_invariant, SMRHN.PlusU1.YYsol, SMRHN.PlusU1.ElevenPlane.Bi_sum_quad, SMRHN.familyUniversal_accGrav, SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂, SMRHN.PlusU1.Y.add_AFL_cube, SMRHN.chargesMapOfSpeciesMap_apply, SMRHN.SM.PlaneSeven.B₀_Bi_cubic, SMνCharges_numberCharges, SMRHN.PlusU1_quadraticACCs, SMRHN.SM.PlaneSeven.B₂_cubic, SMRHN.sum_familyUniversal, SMRHN.PlusU1.QuadSolToSol.cube_α₁_α₂_zero, SMRHN.PlusU1.ElevenPlane.quadCoeff_eq_bilinear, SMRHN.PlusU1.Y.on_cubeTriLin'_ALQ, SMRHN.SM.PlaneSeven.B₂_Bi_cubic, SMνCharges.toSpeciesEquiv_symm_apply, SMRHN.PlusU1.cubeSol, SMRHN.SM.PlaneSeven.B₄_cubic, SMRHN.SM_cubicACC_apply, SMRHN.PlusU1.SU2Sol, SMRHN.SMNoGrav.SU3Sol, SMνACCs.accSU2_decomp, SMRHN.SMNoGrav.cubeSol, SMRHN.PlusU1.BL.add_AFL_quad, SMνACCs.cubeTriLin_toFun_apply_apply, SMRHN.PlusU1.Y.add_AFQ_cube, SMRHN.PlusU1.QuadSol.add_AFL_quad, SMνACCs.accGrav_decomp, SMRHN.sum_familyUniversal_two, SMRHN.SM.PlaneSeven.B₁_cubic, SMRHN.PlusU1.BL.on_quadBiLin, SMRHN.familyUniversal_accQuad, SMRHN.familyUniversal_accSU3, SMRHN.PlusU1.Y.on_cubeTriLin_AFL, SMRHN.familyUniversal_cubeTriLin', SMνCharges.toSpecies_apply, SMRHN.accCube_invariant, SMRHN.accYY_invariant, SMRHN.PlusU1.BL.on_cubeTriLin_AFL, SMRHN.PlusU1.SU3Sol, SMRHN.familyUniversal_accYY, SMRHN.PlusU1.Y.add_quad, SMRHN.familyUniversal_cubeTriLin, SMνACCs.accYY_decomp, SMRHN.PlusU1.quadSol
SMνSpecies 📖	CompOp	29 math math: SMRHN.sum_familyUniversal_one, SMRHN.toSpecies_familyUniversal, SMRHN.sum_familyUniversal_three, SMRHN.familyUniversal_quadBiLin, SMRHN.repCharges_toSpecies, SMνACCs.accCube_decomp, SMνACCs.quadBiLin_decomp, SMνACCs.accSU3_decomp, SMνCharges.toSMSpecies_toSpecies_inv, SMνCharges.toSpecies_one, SMνACCs.cubeTriLin_decomp, SMRHN.speciesFamilyProj_apply, SMνACCs.accQuad_decomp, SMRHN.chargesMapOfSpeciesMap_toSpecies, SMRHN.speciesEmbed_apply, SMRHN.toSpecies_sum_invariant, SMνCharges.charges_eq_toSpecies_eq, SMRHN.chargeMap_apply, SMRHN.chargesMapOfSpeciesMap_apply, SMRHN.speciesFamilyUniversial_apply, SMRHN.sum_familyUniversal, SMνACCs.accSU2_decomp, SMνSpecies_numberCharges, SMνACCs.accGrav_decomp, SMRHN.sum_familyUniversal_two, SMRHN.familyUniversal_cubeTriLin', SMνCharges.toSpecies_apply, SMRHN.familyUniversal_cubeTriLin, SMνACCs.accYY_decomp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SMνCharges_numberCharges 📖	mathematical	—	ACCSystemCharges.numberCharges SMνCharges	—	—
SMνSpecies_numberCharges 📖	mathematical	—	ACCSystemCharges.numberCharges SMνSpecies	—	—

---

← Back to Index