Theorems · Theorem · group theory
Equiv.Perm.mclosure_isSwap
∀ {α : Type u} [inst : DecidableEq α] [Finite α], Submonoid.closure {σ | σ.IsSwap} = ⊤- Defined in
- Mathlib.GroupTheory.Perm.Sign
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- DecidableEqFinite
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Top.topstatement and proof · cited by 9,680
- Fintypeproof · cited by 7,736
- Set.ofPredstatement and proof · cited by 6,101
- Submonoidstatement · cited by 3,086
- Finitestatement and proof · cited by 3,029
- Equiv.Permstatement and proof · cited by 1,375
- Subtype.propproof · cited by 505
- nonempty_fintypeproof · cited by 261
- Submonoid.closurestatement and proof · cited by 167
- top_uniqueproof · cited by 102
- Submonoid.subset_closureproof · cited by 46
- Equiv.Perm.IsSwapstatement and proof · cited by 35
Cited by2
Results whose statement or proof uses this declaration.
- Equiv.Perm.closure_isSwapproof · cited by 3
- Equiv.Perm.mclosure_swap_castSucc_succproof · cited by 0