Files

mathcomp

algebra
- algebraic_hierarchy
- numeric_hierarchy
  - numdomain
  - numfield
  - orderedzmod
  - ssrnum
- algebra
- all_algebra
- archimedean
- arithmetic_tactic
- binnums
- countalg
- field_tactic
- finalg
- fraction
- intdiv
- interval
- interval_inference
- lra
- matrix
- mxalgebra
- mxpoly
- mxred
- poly
- polyXY
- polydiv
- qpoly
- rat
- ring
- ring_quotient
- ring_tactic
- sesquilinear
- spectral
- ssrint
- tensor
- vector
- zmodp
all
- all
boot
- all_boot
- bigop
- binomial
- boot
- choice
- div
- eqtype
- finfun
- fingraph
- finset
- fintype
- generic_quotient
- monoid
- nmodule
- path
- prime
- seq
- ssrAC
- ssrbool
- ssreflect
- ssrfun
- ssrmatching
- ssrnat
- ssrnotations
- tuple
field
- algC
- algebraics_fundamentals
- algnum
- all_field
- closed_field
- cyclotomic
- falgebra
- field
- fieldext
- finfield
- galois
- qfpoly
- separable
finite_group
- action
- all_fingroup
- automorphism
- fingroup
- finite_group
- gproduct
- morphism
- perm
- presentation
- quotient
group_representation
order
- all_order
- order
- preorder
solvable
- abelian
- all_solvable
- alt
- burnside_app
- center
- commutator
- cyclic
- extraspecial
- extremal
- finmodule
- frobenius
- gfunctor
- gseries
- hall
- jordanholder
- maximal
- nilpotent
- pgroup
- primitive_action
- solvable
- sylow
ssreflect
- all_ssreflect

Module mathcomp.test_suite.imset2_gproduct

From mathcomp Require Import boot finite_group.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope group_scope.
Open Scope group_scope.
Check @ker_sdprodm.