Theorems · Definition · group theory

alternatingGroup.ofSubtype

{α : Type u_1} →
  [inst : Fintype α] → [inst_1 : DecidableEq α] → (s : Finset α) → ↥(alternatingGroup ↥s) →* ↥(alternatingGroup α)

The element of alternatingGroup α induced by an element of alternatingGroup s, when s : Finset α.

Defined in

Mathlib.GroupTheory.SpecificGroups.Alternating

Cited by

9 results in Mathlib

Foundations

Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableEq