diff options
Diffstat (limited to 'mathcomp/test_suite/imset2_gproduct.v.out')
| -rw-r--r-- | mathcomp/test_suite/imset2_gproduct.v.out | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/mathcomp/test_suite/imset2_gproduct.v.out b/mathcomp/test_suite/imset2_gproduct.v.out new file mode 100644 index 0000000..673c27c --- /dev/null +++ b/mathcomp/test_suite/imset2_gproduct.v.out @@ -0,0 +1,6 @@ +ker_sdprodm + : forall (gT rT : finGroupType) (H K G : {group gT}) + (fH : {morphism H >-> rT}) (fK : {morphism K >-> rT}) + (eqHK_G : H ><| K = G) (actf : {in H & K, morph_act 'J 'J fH fK}), + 'ker (sdprodm eqHK_G actf) = + [set a * b^-1 | a in H, b in K & fH a == fK b] |