Documentation Verification Report

Centralizer

📁 Source: Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean

Statistics

Metric	Count
Definitions	0
Theorems `card_of_cycleType`, `card_of_cycleType_mul_eq`, `card_of_cycleType_singleton`, `map_subtype_of_cycleType`, `mem_commutatorSet_alternatingGroup`, `mem_commutator_alternatingGroup`, `kerParam_range_eq_centralizer_of_count_le_one`, `odd_of_centralizer_le_alternatingGroup`, `card_le_of_centralizer_le_alternating`, `centralizer_le_alternating_iff`, `count_le_one_of_centralizer_le_alternating`, `commutator_perm_eq`, `commutator_perm_le`, `commutator_alternatingGroup_eq_self`, `commutator_alternatingGroup_eq_top`	15
Total	15

AlternatingGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_of_cycleType` 📖	mathematical	—	`Finset.card` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Finset.filter` `Multiset` `Equiv.Perm.cycleType` `Multiset.decidableEq` `Finset.univ` `alternatingGroup.instFintype` `Multiset.sum` `Nat.instAddCommMonoid` `Fintype.card` `Even` `Multiset.card` `Multiset.decidableDforallMultiset` `Nat.instDecidablePredEven` `Nat.factorial` `Multiset.prod` `Nat.instCommMonoid` `Finset.prod` `Multiset.toFinset` `Multiset.count`	—	`Finset.card_map` `map_subtype_of_cycleType` `Equiv.Perm.card_of_cycleType` `mul_assoc` `Finset.card_empty` `not_and_or`
`card_of_cycleType_mul_eq` 📖	mathematical	—	`Finset.card` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Finset.filter` `Multiset` `Equiv.Perm.cycleType` `Multiset.decidableEq` `Finset.univ` `alternatingGroup.instFintype` `Nat.factorial` `Fintype.card` `Multiset.sum` `Nat.instAddCommMonoid` `Multiset.prod` `Nat.instCommMonoid` `Finset.prod` `Multiset.toFinset` `Multiset.count` `Even` `Multiset.card` `Multiset.decidableDforallMultiset` `Nat.instDecidablePredEven`	—	`Finset.card_map` `map_subtype_of_cycleType` `Finset.card_empty` `ite_mul` `MulZeroClass.zero_mul` `ite_and` `Equiv.Perm.card_of_cycleType_mul_eq`
`card_of_cycleType_singleton` 📖	mathematical	`Fintype.card`	`Finset.card` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Finset.filter` `Multiset` `Equiv.Perm.cycleType` `Multiset.instSingleton` `Multiset.decidableEq` `Finset.univ` `alternatingGroup.instFintype` `Odd` `Nat.instSemiring` `Nat.instDecidablePredOdd` `Nat.factorial` `Nat.choose`	—	`Finset.card_map` `map_subtype_of_cycleType` `Multiset.sum_singleton` `Multiset.card_singleton` `Equiv.Perm.card_of_cycleType_singleton`
`map_subtype_of_cycleType` 📖	mathematical	—	`Finset.map` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Function.Embedding.subtype` `Finset.filter` `Multiset` `Equiv.Perm.cycleType` `Multiset.decidableEq` `Finset.univ` `alternatingGroup.instFintype` `Finset` `Even` `Multiset.sum` `Nat.instAddCommMonoid` `Multiset.card` `Nat.instDecidablePredEven` `Equiv.instFintype` `Finset.instEmptyCollection`	—	`Finset.ext` `Equiv.Perm.sign_of_cycleType` `Even.neg_one_pow` `Finset.eq_empty_iff_forall_notMem` `neg_one_pow_eq_one_iff_even` `Int.instCharZero`

Equiv.Perm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_le_of_centralizer_le_alternating` 📖	mathematical	`Subgroup` `Equiv.Perm` `permGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `alternatingGroup`	`Fintype.card` `Multiset.sum` `Nat.instAddCommMonoid` `cycleType`	—	`card_fixedPoints` `sum_cycleType` `Finset.card_le_univ` `Fintype.exists_pair_of_one_lt_card` `OnCycleFactors.sign_kerParam_apply_apply` `sign_swap'` `Finset.prod_congr` `sign_one` `Finset.prod_const_one` `mul_one` `Int.instCharZero` `OnCycleFactors.kerParam_range_le_centralizer` `Set.mem_range_self`
`centralizer_le_alternating_iff` 📖	mathematical	—	`Subgroup` `Equiv.Perm` `permGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `alternatingGroup` `Odd` `Nat.instSemiring` `Fintype.card` `Multiset.sum` `Nat.instAddCommMonoid` `cycleType` `Multiset.count`	—	`SetLike.le_def` `instIsConcreteLE` `OnCycleFactors.odd_of_centralizer_le_alternatingGroup` `card_le_of_centralizer_le_alternating` `count_le_one_of_centralizer_le_alternating` `MonoidHom.mem_range` `OnCycleFactors.kerParam_range_eq_centralizer_of_count_le_one` `mem_alternatingGroup` `OnCycleFactors.sign_kerParam_apply_apply` `Finset.prod_eq_one` `Subtype.prop` `map_zpow` `MonoidHom.instMonoidHomClass` `IsCycle.sign` `mem_cycleFactorsFinset_iff` `Odd.neg_one_pow` `cycleType_def` `Multiset.mem_map` `neg_neg` `one_zpow` `card_fixedPoints` `card_support_le_one` `le_trans` `Finset.card_le_univ` `sign_one` `mul_one`
`count_le_one_of_centralizer_le_alternating` 📖	mathematical	`Subgroup` `Equiv.Perm` `permGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `alternatingGroup`	`Multiset.count` `cycleType`	—	`Multiset.nodup_iff_count_le_one` `cycleType_def` `Multiset.nodup_map_iff_inj_on` `Finset.nodup` `Mathlib.Tactic.Push.not_forall_eq` `Basis.nonempty` `Equiv.swap_apply_left` `Equiv.swap_apply_right` `Equiv.swap_apply_of_ne_of_ne` `Multiset.eq_replicate_card` `pow_prime_eq_one_iff` `Nat.fact_prime_two` `Subgroup.coe_pow` `Subgroup.coe_one` `map_pow` `MonoidHom.instMonoidHomClass` `Equiv.swap_mul_self` `MonoidHom.map_one` `sign_of_cycleType` `Multiset.sum_replicate` `Multiset.card_replicate` `pow_add` `Even.neg_pow` `Distrib.leftDistribClass` `Nat.instAtLeastTwoHAddOfNat` `one_pow` `one_mul` `Odd.neg_one_pow` `OnCycleFactors.odd_of_centralizer_le_alternatingGroup` `sum_cycleType` `Nat.instCharZero` `Basis.ofPermHom_mem_centralizer` `Basis.card_ofPermHom_support` `Subtype.coe_ne_coe` `Finset.sum_congr` `support_swap` `Finset.sum_insert` `Finset.sum_singleton` `mul_two` `units_ne_neg_self` `Int.instCharZero` `Subtype.prop`

Equiv.Perm.IsThreeCycle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_commutatorSet_alternatingGroup` 📖	mathematical	`Fintype.card` `Equiv.Perm.IsThreeCycle` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup`	`Set` `Set.instMembership` `commutatorSet` `Subgroup.toGroup`	—	`mem_commutatorSet_of_isConj_sq` `alternatingGroup.isThreeCycle_isConj` `congr_simp` `sq` `isThreeCycle_sq`
`mem_commutator_alternatingGroup` 📖	mathematical	`Fintype.card` `Equiv.Perm.IsThreeCycle` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup`	`Subgroup.toGroup` `commutator`	—	`commutator_eq_closure` `Subgroup.subset_closure` `mem_commutatorSet_alternatingGroup`

Equiv.Perm.OnCycleFactors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`kerParam_range_eq_centralizer_of_count_le_one` 📖	mathematical	`Multiset.count` `Equiv.Perm.cycleType`	`MonoidHom.range` `Equiv.Perm` `Set.Elem` `Function.fixedPoints` `DFunLike.coe` `EquivLike.toFunLike` `Equiv.instEquivLike` `Prod.instGroup` `Equiv.Perm.permGroup` `Pi.group` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Equiv.Perm.cycleFactorsFinset` `Subgroup` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `kerParam` `Subgroup.centralizer` `Set` `Set.instSingletonSet`	—	`Subgroup.ext` `kerParam_range_le_centralizer` `kerParam_range_eq` `Equiv.Perm.ext` `Multiset.nodup_map_iff_inj_on` `Finset.nodup` `Equiv.Perm.cycleType_def` `Multiset.nodup_iff_count_le_one` `Subtype.prop` `mem_range_toPermHom_iff`
`odd_of_centralizer_le_alternatingGroup` 📖	mathematical	`Subgroup` `Equiv.Perm` `Equiv.Perm.permGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.centralizer` `Set` `Set.instSingletonSet` `alternatingGroup` `Multiset` `Multiset.instMembership` `Equiv.Perm.cycleType`	`Odd` `Nat.instSemiring`	—	`Multiset.mem_map` `Equiv.Perm.cycleType_def` `Subgroup.mem_centralizer_singleton_iff` `Equiv.Perm.self_mem_cycle_factors_commute` `Finset.mem_def` `Nat.not_even_iff_odd` `Int.units_ne_iff_eq_neg` `neg_eq_iff_eq_neg` `Equiv.Perm.IsCycle.sign` `Equiv.Perm.mem_cycleFactorsFinset_iff` `Even.neg_one_pow`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commutator_alternatingGroup_eq_self` 📖	mathematical	`Fintype.card`	`Bracket.bracket` `Subgroup` `Equiv.Perm` `Equiv.Perm.permGroup` `Subgroup.commutator` `alternatingGroup`	—	`Subgroup.map_subtype_commutator` `commutator_alternatingGroup_eq_top` `MonoidHom.range_eq_map` `Subgroup.range_subtype`
`commutator_alternatingGroup_eq_top` 📖	mathematical	`Fintype.card`	`commutator` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `Top.top` `Subgroup.instTop`	—	`Equiv.Perm.closure_three_cycles_eq_alternating` `Subgroup.closure_closure_coe_preimage` `eq_top_iff` `Subgroup.closure_le` `Equiv.Perm.IsThreeCycle.mem_commutator_alternatingGroup`

alternatingGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`commutator_perm_eq` 📖	mathematical	`Fintype.card`	`commutator` `Equiv.Perm` `Equiv.Perm.permGroup` `alternatingGroup`	—	`le_antisymm` `commutator_perm_le` `commutator_alternatingGroup_eq_self` `Subgroup.commutator_mono` `le_top`
`commutator_perm_le` 📖	mathematical	—	`Subgroup` `Equiv.Perm` `Equiv.Perm.permGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `commutator` `alternatingGroup`	—	`commutator_eq_closure` `map_commutatorElement` `MonoidHom.instMonoidHomClass`

---

← Back to Index