K (Definitions)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Notations |
K (Definitions)
kAut [def, in mathcomp.field.galois]ker [def, in mathcomp.finite_group.morphism]
ker_cprod_by [def, in mathcomp.solvable.center]
ker_cprod_by_group [def, in mathcomp.solvable.center]
ker_group [def, in mathcomp.finite_group.morphism]
ker_sub_ahom_aspace [def, in mathcomp.field.falgebra]
kermx [def, in mathcomp.algebra.mxalgebra]
kermxpoly [def, in mathcomp.algebra.mxpoly]
kHom [def, in mathcomp.field.galois]
kHom_is_additive [def, in mathcomp.field.galois]
kHom_is_multiplicative [def, in mathcomp.field.galois]
kHom_rmorphism [def, in mathcomp.field.galois]
kHomExtend [def, in mathcomp.field.galois]
kquo_mx [def, in mathcomp.group_representation.mxrepresentation]
kquo_repr [def, in mathcomp.group_representation.mxrepresentation]