Documentation Verification Report

LinearMaps

📁 Source: PhysLean/Mathematics/LinearMaps.lean

Statistics

Metric	Count
Definitions `BiLinearSymm`, `instFun`, `mk₂`, `toHomogeneousQuad`, `toLinearMap`, `toLinear₁`, `HomogeneousCubic`, `instFun`, `HomogeneousQuadratic`, `instFun`, `IsSymmetric`, `TriLinearSymm`, `instFun`, `mk₃`, `toCubic`, `toLinearMap`, `toLinear₁`	17
Theorems `map_add₁`, `map_add₂`, `map_smul₁`, `map_smul₂`, `map_sum₁`, `map_sum₂`, `mk₂_toFun_apply`, `swap`, `swap'`, `toHomogeneousQuad_add`, `toHomogeneousQuad_apply`, `toLinear₁_apply`, `map_smul`, `map_smul`, `swap`, `map_add₁`, `map_add₂`, `map_add₃`, `map_smul₁`, `map_smul₂`, `map_smul₃`, `map_sum₁`, `map_sum₁₂₃`, `map_sum₂`, `map_sum₃`, `mk₃_toFun_apply_apply`, `swap₁`, `swap₁'`, `swap₂`, `swap₂'`, `swap₃`, `toCubic_add`, `toCubic_apply`, `toLinear₁_apply`	34
Total	51

BiLinearSymm

Definitions

Name	Category	Theorems
`instFun` 📖	CompOp	43 math math: `toLinear₁_apply`, `MSSMACC.α₃_proj`, `SMACCs.quadBiLin_toFun_apply`, `toHomogeneousQuad_apply`, `mk₂_toFun_apply`, `MSSMACC.AnomalyFreePerp.perpB₃`, `SMRHN.familyUniversal_quadBiLin`, `SMRHN.PlusU1.ElevenPlane.Bi_Bj_quad`, `SMRHN.PlusU1.Y.on_quadBiLin_AFL`, `map_smul₁`, `SMνACCs.quadBiLin_decomp`, `map_add₁`, `MSSMACC.proj_val`, `map_smul₂`, `MSSMACC.α₁_proj`, `swap`, `MSSMACC.α₂_proj`, `SMRHN.PlusU1.Y.on_quadBiLin`, `SMRHN.PlusU1.BL.on_quadBiLin_AFL`, `SMνACCs.quadBiLin_toFun_apply`, `MSSMACC.dot_toFun_apply`, `MSSMACC.AnomalyFreePerp.perpY₃`, `MSSMACC.planeY₃B₃_quad`, `MSSMACC.lineQuad_cube`, `MSSMACC.cube_proj_proj_B₃`, `MSSMACC.cube_proj_proj_Y₃`, `SMRHN.PlusU1.ElevenPlane.Bi_sum_quad`, `MSSMACC.quad_self_proj`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `map_add₂`, `map_sum₂`, `SMRHN.PlusU1.ElevenPlane.quadCoeff_eq_bilinear`, `MSSMACCs.quadBiLin_toFun_apply`, `MSSMACC.quad_B₃_proj`, `map_sum₁`, `toHomogeneousQuad_add`, `MSSMACC.cube_proj_proj_self`, `MSSMACC.cube_proj`, `SMRHN.PlusU1.QuadSol.add_AFL_quad`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `SMRHN.PlusU1.BL.on_quadBiLin`, `MSSMACC.quad_proj`
`mk₂` 📖	CompOp	1 math math: `mk₂_toFun_apply`
`toHomogeneousQuad` 📖	CompOp	4 math math: `toHomogeneousQuad_apply`, `MSSMACC_quadraticACCs`, `SMRHN.PlusU1_quadraticACCs`, `toHomogeneousQuad_add`
`toLinearMap` 📖	CompOp	1 math math: `swap'`
`toLinear₁` 📖	CompOp	1 math math: `toLinear₁_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_add₁` 📖	mathematical	—	`BiLinearSymm` `instFun`	—	—
`map_add₂` 📖	mathematical	—	`BiLinearSymm` `instFun`	—	`swap` `map_add₁`
`map_smul₁` 📖	mathematical	—	`BiLinearSymm` `instFun`	—	—
`map_smul₂` 📖	mathematical	—	`BiLinearSymm` `instFun`	—	`swap` `map_smul₁`
`map_sum₁` 📖	mathematical	—	`BiLinearSymm` `instFun`	—	—
`map_sum₂` 📖	mathematical	—	`BiLinearSymm` `instFun`	—	—
`mk₂_toFun_apply` 📖	mathematical	—	`BiLinearSymm` `instFun` `mk₂`	—	—
`swap` 📖	mathematical	—	`BiLinearSymm` `instFun`	—	`swap'`
`swap'` 📖	mathematical	—	`toLinearMap`	—	—
`toHomogeneousQuad_add` 📖	mathematical	—	`HomogeneousQuadratic` `HomogeneousQuadratic.instFun` `toHomogeneousQuad` `BiLinearSymm` `instFun`	—	`map_add₁` `swap`
`toHomogeneousQuad_apply` 📖	mathematical	—	`toHomogeneousQuad` `BiLinearSymm` `instFun`	—	—
`toLinear₁_apply` 📖	mathematical	—	`BiLinearSymm` `instFun` `toLinear₁`	—	—

HomogeneousCubic

Definitions

Name	Category	Theorems
`instFun` 📖	CompOp	42 math math: `MSSMACCs.accCube_ext`, `MSSM.accCube_invariant`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube`, `SMνACCs.accCube_decomp`, `PureU1.Even.parameterizationCharge_cube`, `SMRHN.SM.cubeSol`, `PureU1.VectorLikeOddPlane.P_accCube`, `SMACCs.accCube_ext`, `ACCSystemGroupAction.cubicInvariant`, `map_smul`, `PureU1.Three.cube_for_linSol'`, `SMνACCs.accCube_ext`, `MSSMACC.planeY₃B₃_cubic`, `SMRHN.SM.PlaneSeven.B_in_accCube`, `PureU1.VectorLikeEvenPlane.basis_accCube`, `SM.accCube_invariant`, `PureU1.accCube_explicit`, `SMRHN.PlusU1.Y.add_AF_cube`, `MSSMACC.lineQuad_cube`, `PureU1.VectorLikeEvenPlane.P_accCube`, `PureU1.accCube_invariant`, `SMRHN.familyUniversal_accCube`, `PureU1.VectorLikeEvenPlane.basis!_accCube`, `SMRHN.PlusU1.BL.add_AFL_cube`, `PureU1.Three.cube_for_linSol`, `SMRHN.PlusU1.Y.add_AFL_cube`, `TriLinearSymm.toCubic_add`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_cube`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `PureU1.VectorLikeEvenPlane.P!_accCube`, `SMRHN.PlusU1.QuadSolToSol.cube_α₁_α₂_zero`, `MSSMACC.lineY₃B₃Charges_cubic`, `PureU1.VectorLikeOddPlane.P!_accCube`, `SMRHN.PlusU1.cubeSol`, `PureU1.Odd.parameterizationCharge_cube`, `SMRHN.SMNoGrav.cubeSol`, `SMRHN.PlusU1.Y.add_AFQ_cube`, `SM.SMNoGrav.cubeSol`, `SMRHN.accCube_invariant`, `ACCSystem.Sols.cubicSol`, `SM.SMNoGrav.One.linearParameters.cubic`, `MSSMACC.lineCube_cube`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_smul` 📖	mathematical	—	`HomogeneousCubic` `instFun`	—	—

HomogeneousQuadratic

Definitions

Name	Category	Theorems
`instFun` 📖	CompOp	27 math math: `map_smul`, `MSSM.accQuad_invariant`, `SMRHN.PlusU1.ElevenPlane.on_accQuad`, `ACCSystemGroupAction.quadInvariant`, `SMRHN.PlusU1.BL.add_quad`, `SM.accQuad_invariant`, `SMνACCs.accQuad_decomp`, `ACCSystemQuad.QuadSols.quadSol`, `SMRHN.PlusU1.Y.on_cubeTriLin'`, `MSSMACC.lineQuadAFL_quad`, `MSSMACC.planeY₃B₃_quad`, `SMνACCs.accQuad_ext`, `MSSMACC.lineCube_quad`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `SMRHN.PlusU1.Y.add_AFL_quad`, `SMRHN.accQuad_invariant`, `MSSMACC.quadSol`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂`, `SMACCs.accQuad_ext`, `MSSMACCs.accQuad_ext`, `MSSMACC.lineY₃B₃Charges_quad`, `BiLinearSymm.toHomogeneousQuad_add`, `SMRHN.PlusU1.BL.add_AFL_quad`, `SMRHN.PlusU1.QuadSol.add_AFL_quad`, `SMRHN.familyUniversal_accQuad`, `SMRHN.PlusU1.Y.add_quad`, `SMRHN.PlusU1.quadSol`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_smul` 📖	mathematical	—	`HomogeneousQuadratic` `instFun`	—	—

IsSymmetric

Theorems

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

TriLinearSymm

Definitions

Name	Category	Theorems
`instFun` 📖	CompOp	75 math math: `SMRHN.SM.PlaneSeven.Bi_Bj_ne_cubic`, `MSSMACC.α₃_proj`, `PureU1.accCubeTriLinSymm_toFun_apply_apply`, `PureU1.Even.line_in_cubic_P_P_P!`, `PureU1.Odd.parameterizationAsLinear_val`, `PureU1.Even.lineInCubicPerm_swap`, `SMRHN.SM.PlaneSeven.B₄_Bi_cubic`, `SMRHN.PlusU1.BL.on_cubeTriLin`, `SMRHN.SM.PlaneSeven.B₅_Bi_cubic`, `PureU1.Odd.P_P_P!_accCube'`, `swap₃`, `swap₂`, `SMRHN.SM.PlaneSeven.Bi_Bi_Bj_cubic`, `SMRHN.SM.PlaneSeven.B₃_cubic`, `SMνACCs.cubeTriLin_decomp`, `PureU1.Even.anomalyFree_param`, `map_smul₁`, `SMRHN.SM.PlaneSeven.Bi_Bj_Bk_cubic`, `map_sum₃`, `MSSMACC.doublePoint_Y₃_B₃`, `SMRHN.SM.PlaneSeven.B₆_Bi_cubic`, `PureU1.VectorLikeOddPlane.P_P_P!_accCube`, `map_sum₁`, `PureU1.Odd.line_in_cubic_P_P_P!`, `SMACCs.cubeTriLin_toFun_apply_apply`, `PureU1.Even.parameterizationAsLinear_val`, `MSSMACC.planeY₃B₃_cubic`, `MSSMACC.lineY₃B₃_doublePoint`, `SMRHN.PlusU1.Y.on_cubeTriLin`, `SMRHN.SM.PlaneSeven.B₅_cubic`, `toCubic_apply`, `SMRHN.PlusU1.Y.on_cubeTriLin'`, `PureU1.VectorLikeEvenPlane.P_P_P!_accCube`, `map_add₃`, `PureU1.Odd.anomalyFree_param`, `map_sum₂`, `MSSMACC.cube_proj_proj_B₃`, `SMRHN.SM.PlaneSeven.B₃_Bi_cubic`, `PureU1.Odd.lineInCubic_expand`, `MSSMACC.cube_proj_proj_Y₃`, `swap₁`, `MSSMACC.lineCube_quad`, `SMRHN.SM.PlaneSeven.B₆_cubic`, `MSSMACC.doublePoint_Y₃_Y₃`, `SMRHN.PlusU1.BL.add_AFL_cube`, `SMRHN.SM.PlaneSeven.B₀_cubic`, `SMRHN.SM.PlaneSeven.B₁_Bi_cubic`, `SMRHN.PlusU1.Y.add_AFL_cube`, `toCubic_add`, `SMRHN.SM.PlaneSeven.B₀_Bi_cubic`, `SMRHN.SM.PlaneSeven.B₂_cubic`, `map_add₁`, `SMRHN.PlusU1.Y.on_cubeTriLin'_ALQ`, `SMRHN.SM.PlaneSeven.B₂_Bi_cubic`, `SMRHN.SM.PlaneSeven.B₄_cubic`, `map_smul₃`, `PureU1.Odd.lineInCubicPerm_swap`, `map_smul₂`, `MSSMACC.cube_proj_proj_self`, `SMνACCs.cubeTriLin_toFun_apply_apply`, `map_sum₁₂₃`, `MSSMACC.cube_proj`, `MSSMACC.doublePoint_B₃_B₃`, `PureU1.VectorLikeEvenPlane.P_P!_P!_accCube`, `SMRHN.SM.PlaneSeven.B₁_cubic`, `SMRHN.PlusU1.Y.on_cubeTriLin_AFL`, `PureU1.Even.P_P_P!_accCube'`, `MSSMACCs.cubeTriLin_toFun_apply_apply`, `SMRHN.familyUniversal_cubeTriLin'`, `SMRHN.PlusU1.BL.on_cubeTriLin_AFL`, `PureU1.Even.lineInCubic_expand`, `toLinear₁_apply`, `mk₃_toFun_apply_apply`, `map_add₂`, `SMRHN.familyUniversal_cubeTriLin`
`mk₃` 📖	CompOp	1 math math: `mk₃_toFun_apply_apply`
`toCubic` 📖	CompOp	2 math math: `toCubic_apply`, `toCubic_add`
`toLinearMap` 📖	CompOp	2 math math: `swap₁'`, `swap₂'`
`toLinear₁` 📖	CompOp	1 math math: `toLinear₁_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_add₁` 📖	mathematical	—	`TriLinearSymm` `instFun`	—	—
`map_add₂` 📖	mathematical	—	`TriLinearSymm` `instFun`	—	`swap₁` `map_add₁`
`map_add₃` 📖	mathematical	—	`TriLinearSymm` `instFun`	—	`swap₃` `map_add₁`
`map_smul₁` 📖	mathematical	—	`TriLinearSymm` `instFun`	—	—
`map_smul₂` 📖	mathematical	—	`TriLinearSymm` `instFun`	—	`swap₁` `map_smul₁`
`map_smul₃` 📖	mathematical	—	`TriLinearSymm` `instFun`	—	`swap₃` `map_smul₁`
`map_sum₁` 📖	mathematical	—	`TriLinearSymm` `instFun`	—	`toLinear₁_apply`
`map_sum₁₂₃` 📖	mathematical	—	`TriLinearSymm` `instFun`	—	`map_sum₁` `map_sum₂` `map_sum₃`
`map_sum₂` 📖	mathematical	—	`TriLinearSymm` `instFun`	—	`swap₁` `map_sum₁`
`map_sum₃` 📖	mathematical	—	`TriLinearSymm` `instFun`	—	—
`mk₃_toFun_apply_apply` 📖	mathematical	—	`TriLinearSymm` `instFun` `mk₃`	—	—
`swap₁` 📖	mathematical	—	`TriLinearSymm` `instFun`	—	`swap₁'`
`swap₁'` 📖	mathematical	—	`toLinearMap`	—	—
`swap₂` 📖	mathematical	—	`TriLinearSymm` `instFun`	—	`swap₂'`
`swap₂'` 📖	mathematical	—	`toLinearMap`	—	—
`swap₃` 📖	mathematical	—	`TriLinearSymm` `instFun`	—	`swap₁` `swap₂`
`toCubic_add` 📖	mathematical	—	`HomogeneousCubic` `HomogeneousCubic.instFun` `toCubic` `TriLinearSymm` `instFun`	—	`map_add₁` `map_add₂` `map_add₃` `swap₂` `swap₁`
`toCubic_apply` 📖	mathematical	—	`toCubic` `TriLinearSymm` `instFun`	—	—
`toLinear₁_apply` 📖	mathematical	—	`TriLinearSymm` `instFun` `toLinear₁`	—	—

(root)

Definitions

Name	Category	Theorems
`BiLinearSymm` 📖	CompData	43 math math: `BiLinearSymm.toLinear₁_apply`, `MSSMACC.α₃_proj`, `SMACCs.quadBiLin_toFun_apply`, `BiLinearSymm.toHomogeneousQuad_apply`, `BiLinearSymm.mk₂_toFun_apply`, `MSSMACC.AnomalyFreePerp.perpB₃`, `SMRHN.familyUniversal_quadBiLin`, `SMRHN.PlusU1.ElevenPlane.Bi_Bj_quad`, `SMRHN.PlusU1.Y.on_quadBiLin_AFL`, `BiLinearSymm.map_smul₁`, `SMνACCs.quadBiLin_decomp`, `BiLinearSymm.map_add₁`, `MSSMACC.proj_val`, `BiLinearSymm.map_smul₂`, `MSSMACC.α₁_proj`, `BiLinearSymm.swap`, `MSSMACC.α₂_proj`, `SMRHN.PlusU1.Y.on_quadBiLin`, `SMRHN.PlusU1.BL.on_quadBiLin_AFL`, `SMνACCs.quadBiLin_toFun_apply`, `MSSMACC.dot_toFun_apply`, `MSSMACC.AnomalyFreePerp.perpY₃`, `MSSMACC.planeY₃B₃_quad`, `MSSMACC.lineQuad_cube`, `MSSMACC.cube_proj_proj_B₃`, `MSSMACC.cube_proj_proj_Y₃`, `SMRHN.PlusU1.ElevenPlane.Bi_sum_quad`, `MSSMACC.quad_self_proj`, `MSSMACC.Y₃_plus_B₃_plus_proj`, `BiLinearSymm.map_add₂`, `BiLinearSymm.map_sum₂`, `SMRHN.PlusU1.ElevenPlane.quadCoeff_eq_bilinear`, `MSSMACCs.quadBiLin_toFun_apply`, `MSSMACC.quad_B₃_proj`, `BiLinearSymm.map_sum₁`, `BiLinearSymm.toHomogeneousQuad_add`, `MSSMACC.cube_proj_proj_self`, `MSSMACC.cube_proj`, `SMRHN.PlusU1.QuadSol.add_AFL_quad`, `MSSMACC.lineQuad_val`, `MSSMACC.quad_Y₃_proj`, `SMRHN.PlusU1.BL.on_quadBiLin`, `MSSMACC.quad_proj`
`HomogeneousCubic` 📖	CompOp	42 math math: `MSSMACCs.accCube_ext`, `MSSM.accCube_invariant`, `SMRHN.PlusU1.QuadSolToSol.BL_add_α₁_α₂_cube`, `SMνACCs.accCube_decomp`, `PureU1.Even.parameterizationCharge_cube`, `SMRHN.SM.cubeSol`, `PureU1.VectorLikeOddPlane.P_accCube`, `SMACCs.accCube_ext`, `ACCSystemGroupAction.cubicInvariant`, `HomogeneousCubic.map_smul`, `PureU1.Three.cube_for_linSol'`, `SMνACCs.accCube_ext`, `MSSMACC.planeY₃B₃_cubic`, `SMRHN.SM.PlaneSeven.B_in_accCube`, `PureU1.VectorLikeEvenPlane.basis_accCube`, `SM.accCube_invariant`, `PureU1.accCube_explicit`, `SMRHN.PlusU1.Y.add_AF_cube`, `MSSMACC.lineQuad_cube`, `PureU1.VectorLikeEvenPlane.P_accCube`, `PureU1.accCube_invariant`, `SMRHN.familyUniversal_accCube`, `PureU1.VectorLikeEvenPlane.basis!_accCube`, `SMRHN.PlusU1.BL.add_AFL_cube`, `PureU1.Three.cube_for_linSol`, `SMRHN.PlusU1.Y.add_AFL_cube`, `TriLinearSymm.toCubic_add`, `MSSMACC.AnomalyFreePerp.toSolNSQuad_cube`, `SM.SMNoGrav.One.linearParametersQENeqZero.cubic`, `PureU1.VectorLikeEvenPlane.P!_accCube`, `SMRHN.PlusU1.QuadSolToSol.cube_α₁_α₂_zero`, `MSSMACC.lineY₃B₃Charges_cubic`, `PureU1.VectorLikeOddPlane.P!_accCube`, `SMRHN.PlusU1.cubeSol`, `PureU1.Odd.parameterizationCharge_cube`, `SMRHN.SMNoGrav.cubeSol`, `SMRHN.PlusU1.Y.add_AFQ_cube`, `SM.SMNoGrav.cubeSol`, `SMRHN.accCube_invariant`, `ACCSystem.Sols.cubicSol`, `SM.SMNoGrav.One.linearParameters.cubic`, `MSSMACC.lineCube_cube`
`HomogeneousQuadratic` 📖	CompOp	27 math math: `HomogeneousQuadratic.map_smul`, `MSSM.accQuad_invariant`, `SMRHN.PlusU1.ElevenPlane.on_accQuad`, `ACCSystemGroupAction.quadInvariant`, `SMRHN.PlusU1.BL.add_quad`, `SM.accQuad_invariant`, `SMνACCs.accQuad_decomp`, `ACCSystemQuad.QuadSols.quadSol`, `SMRHN.PlusU1.Y.on_cubeTriLin'`, `MSSMACC.lineQuadAFL_quad`, `MSSMACC.planeY₃B₃_quad`, `SMνACCs.accQuad_ext`, `MSSMACC.lineCube_quad`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂_zero`, `SMRHN.PlusU1.Y.add_AFL_quad`, `SMRHN.accQuad_invariant`, `MSSMACC.quadSol`, `SMRHN.PlusU1.QuadSol.accQuad_α₁_α₂`, `SMACCs.accQuad_ext`, `MSSMACCs.accQuad_ext`, `MSSMACC.lineY₃B₃Charges_quad`, `BiLinearSymm.toHomogeneousQuad_add`, `SMRHN.PlusU1.BL.add_AFL_quad`, `SMRHN.PlusU1.QuadSol.add_AFL_quad`, `SMRHN.familyUniversal_accQuad`, `SMRHN.PlusU1.Y.add_quad`, `SMRHN.PlusU1.quadSol`
`IsSymmetric` 📖	CompData	—
`TriLinearSymm` 📖	CompData	75 math math: `SMRHN.SM.PlaneSeven.Bi_Bj_ne_cubic`, `MSSMACC.α₃_proj`, `PureU1.accCubeTriLinSymm_toFun_apply_apply`, `PureU1.Even.line_in_cubic_P_P_P!`, `PureU1.Odd.parameterizationAsLinear_val`, `PureU1.Even.lineInCubicPerm_swap`, `SMRHN.SM.PlaneSeven.B₄_Bi_cubic`, `SMRHN.PlusU1.BL.on_cubeTriLin`, `SMRHN.SM.PlaneSeven.B₅_Bi_cubic`, `PureU1.Odd.P_P_P!_accCube'`, `TriLinearSymm.swap₃`, `TriLinearSymm.swap₂`, `SMRHN.SM.PlaneSeven.Bi_Bi_Bj_cubic`, `SMRHN.SM.PlaneSeven.B₃_cubic`, `SMνACCs.cubeTriLin_decomp`, `PureU1.Even.anomalyFree_param`, `TriLinearSymm.map_smul₁`, `SMRHN.SM.PlaneSeven.Bi_Bj_Bk_cubic`, `TriLinearSymm.map_sum₃`, `MSSMACC.doublePoint_Y₃_B₃`, `SMRHN.SM.PlaneSeven.B₆_Bi_cubic`, `PureU1.VectorLikeOddPlane.P_P_P!_accCube`, `TriLinearSymm.map_sum₁`, `PureU1.Odd.line_in_cubic_P_P_P!`, `SMACCs.cubeTriLin_toFun_apply_apply`, `PureU1.Even.parameterizationAsLinear_val`, `MSSMACC.planeY₃B₃_cubic`, `MSSMACC.lineY₃B₃_doublePoint`, `SMRHN.PlusU1.Y.on_cubeTriLin`, `SMRHN.SM.PlaneSeven.B₅_cubic`, `TriLinearSymm.toCubic_apply`, `SMRHN.PlusU1.Y.on_cubeTriLin'`, `PureU1.VectorLikeEvenPlane.P_P_P!_accCube`, `TriLinearSymm.map_add₃`, `PureU1.Odd.anomalyFree_param`, `TriLinearSymm.map_sum₂`, `MSSMACC.cube_proj_proj_B₃`, `SMRHN.SM.PlaneSeven.B₃_Bi_cubic`, `PureU1.Odd.lineInCubic_expand`, `MSSMACC.cube_proj_proj_Y₃`, `TriLinearSymm.swap₁`, `MSSMACC.lineCube_quad`, `SMRHN.SM.PlaneSeven.B₆_cubic`, `MSSMACC.doublePoint_Y₃_Y₃`, `SMRHN.PlusU1.BL.add_AFL_cube`, `SMRHN.SM.PlaneSeven.B₀_cubic`, `SMRHN.SM.PlaneSeven.B₁_Bi_cubic`, `SMRHN.PlusU1.Y.add_AFL_cube`, `TriLinearSymm.toCubic_add`, `SMRHN.SM.PlaneSeven.B₀_Bi_cubic`, `SMRHN.SM.PlaneSeven.B₂_cubic`, `TriLinearSymm.map_add₁`, `SMRHN.PlusU1.Y.on_cubeTriLin'_ALQ`, `SMRHN.SM.PlaneSeven.B₂_Bi_cubic`, `SMRHN.SM.PlaneSeven.B₄_cubic`, `TriLinearSymm.map_smul₃`, `PureU1.Odd.lineInCubicPerm_swap`, `TriLinearSymm.map_smul₂`, `MSSMACC.cube_proj_proj_self`, `SMνACCs.cubeTriLin_toFun_apply_apply`, `TriLinearSymm.map_sum₁₂₃`, `MSSMACC.cube_proj`, `MSSMACC.doublePoint_B₃_B₃`, `PureU1.VectorLikeEvenPlane.P_P!_P!_accCube`, `SMRHN.SM.PlaneSeven.B₁_cubic`, `SMRHN.PlusU1.Y.on_cubeTriLin_AFL`, `PureU1.Even.P_P_P!_accCube'`, `MSSMACCs.cubeTriLin_toFun_apply_apply`, `SMRHN.familyUniversal_cubeTriLin'`, `SMRHN.PlusU1.BL.on_cubeTriLin_AFL`, `PureU1.Even.lineInCubic_expand`, `TriLinearSymm.toLinear₁_apply`, `TriLinearSymm.mk₃_toFun_apply_apply`, `TriLinearSymm.map_add₂`, `SMRHN.familyUniversal_cubeTriLin`

---

← Back to Index