Module mathcomp.finite_group.all_fingroup
Attributes deprecated(since="mathcomp 2.6.0",note="'all_fingroup' has been renamed 'finite_group'.").
From mathcomp Require Export finite_group.
Files
mathcomp
algebra
algebraic_hierarchy
numeric_hierarchy
- 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
group_representation
ssreflect
note="'all_fingroup' has been renamed 'finite_group'.").
From mathcomp Require Export finite_group.