mathcomp/test_suite/imset2_gproduct.v


1
2
3
4
5
6
7

From mathcomp Require Import all_ssreflect all_fingroup.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import GroupScope.
Open Scope group_scope.
Check @ker_sdprodm.