Documentation Verification Report

KleinFour

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

Statistics

Metric	Count
Definitions `kleinFour`	1
Theorems `card_of_card_eq_four`, `card_two_sylow_of_card_eq_four`, `characteristic_kleinFour`, `coe_kleinFour_of_card_eq_four`, `coe_two_sylow_of_card_eq_four`, `exponent_kleinFour_of_card_eq_four`, `kleinFour_card_of_card_eq_four`, `kleinFour_eq_commutator`, `kleinFour_isKleinFour`, `mem_kleinFour_of_order_two_pow`, `normal_kleinFour`, `subsingleton_two_sylow`, `two_sylow_eq_kleinFour_of_card_eq_four`	13
Total	14

alternatingGroup

Definitions

Name	Category	Theorems
`kleinFour` 📖	CompOp	8 math math: `kleinFour_card_of_card_eq_four`, `characteristic_kleinFour`, `kleinFour_isKleinFour`, `kleinFour_eq_commutator`, `coe_kleinFour_of_card_eq_four`, `two_sylow_eq_kleinFour_of_card_eq_four`, `normal_kleinFour`, `exponent_kleinFour_of_card_eq_four`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_of_card_eq_four` 📖	mathematical	`Nat.card`	`Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup`	—	`Finite.one_lt_card_iff_nontrivial` `Finite.of_fintype` `Nat.instAtLeastTwoHAddOfNat` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instZeroLEOneClass` `Nat.instCharZero` `nat_card_alternatingGroup`
`card_two_sylow_of_card_eq_four` 📖	mathematical	`Nat.card`	`Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `Sylow.toSubgroup`	—	`Sylow.card_eq_multiplicity` `Subgroup.instFiniteSubtypeMem` `Equiv.finite_left` `Finite.of_fintype` `Nat.fact_prime_two` `card_of_card_eq_four` `Nat.factorization_mul_apply_of_coprime` `Nat.factorization_pow` `Finsupp.coe_smul` `Pi.smul_apply` `smul_eq_mul` `Nat.Prime.factorization_self` `Nat.prime_two` `Nat.factorization_eq_zero_of_not_dvd` `mul_one` `add_zero`
`characteristic_kleinFour` 📖	mathematical	`Nat.card`	`Subgroup.Characteristic` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `kleinFour`	—	`Sylow.nonempty` `subsingleton_two_sylow` `two_sylow_eq_kleinFour_of_card_eq_four` `Sylow.characteristic_of_subsingleton`
`coe_kleinFour_of_card_eq_four` 📖	mathematical	`Nat.card`	`SetLike.coe` `Subgroup` `Equiv.Perm` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `kleinFour` `Set` `Set.instUnion` `Set.instSingletonSet` `Subgroup.one` `setOf` `Multiset` `Equiv.Perm.cycleType` `Multiset.instInsert` `Multiset.instSingleton`	—	`Sylow.nonempty` `two_sylow_eq_kleinFour_of_card_eq_four` `coe_two_sylow_of_card_eq_four`
`coe_two_sylow_of_card_eq_four` 📖	mathematical	`Nat.card`	`SetLike.coe` `Sylow` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `Sylow.instSetLike` `Set` `Set.instUnion` `Set.instSingletonSet` `Subgroup.one` `setOf` `Multiset` `Equiv.Perm.cycleType` `Multiset.instInsert` `Multiset.instSingleton`	—	`Set.eq_of_subset_of_card_le` `IsPGroup.iff_orderOf` `Nat.fact_prime_two` `Sylow.isPGroup'` `orderOf_submonoid` `SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `mem_kleinFour_of_order_two_pow` `Eq.dvd` `Eq.trans_ge` `card_two_sylow_of_card_eq_four` `Nat.card_eq_card_toFinset` `Set.toFinset_union` `Set.toFinset_singleton` `Set.toFinset_setOf` `LE.le.trans` `Finset.card_union_le` `Finset.card_singleton` `AlternatingGroup.card_of_cycleType` `Nat.card_eq_fintype_card`
`exponent_kleinFour_of_card_eq_four` 📖	mathematical	`Nat.card`	`Monoid.exponent` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `kleinFour` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Monoid.exponent_dvd` `coe_kleinFour_of_card_eq_four` `SetLike.mem_coe` `one_pow` `Equiv.Perm.lcm_cycleType` `Multiset.lcm_cons` `Multiset.lcm_singleton` `normalize_eq` `Unique.instSubsingleton` `lcm_same` `pow_orderOf_eq_one` `Nat.dvd_prime` `Nat.prime_two` `Monoid.exp_eq_one_iff` `Finite.card_le_one_iff_subsingleton` `Subgroup.instFiniteSubtypeMem` `Equiv.finite_left` `Finite.of_fintype` `kleinFour_card_of_card_eq_four`
`kleinFour_card_of_card_eq_four` 📖	mathematical	`Nat.card`	`Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `kleinFour`	—	`Sylow.nonempty` `two_sylow_eq_kleinFour_of_card_eq_four` `card_two_sylow_of_card_eq_four`
`kleinFour_eq_commutator` 📖	mathematical	`Nat.card`	`kleinFour` `commutator` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup`	—	`normal_kleinFour` `kleinFour_card_of_card_eq_four` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Subgroup.card_eq_card_quotient_mul_card_subgroup` `card_of_card_eq_four` `Subgroup.Normal.quotient_commutative_iff_commutator_le` `IsCyclic.commutative` `isCyclic_of_prime_card` `Nat.fact_prime_three` `commutator_eq_bot_iff_center_eq_top` `center_eq_bot` `le_of_eq` `bot_ne_top` `Subgroup.nontrivial_iff` `Finite.one_lt_card_iff_nontrivial` `Subgroup.instFiniteSubtypeMem` `Equiv.finite_left` `Finite.of_fintype` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instZeroLEOneClass` `Subgroup.bot_or_exists_ne_one` `Set.mem_setOf_eq` `Set.mem_singleton_iff` `Set.mem_union` `coe_kleinFour_of_card_eq_four` `SetLike.mem_coe` `le_antisymm` `Subgroup.one_mem` `isConj_iff` `Equiv.Perm.isConj_iff_cycleType_eq` `normal` `MulAut.conjNormal_apply` `symm` `IsEquiv.toSymm` `eq_isEquiv` `MonoidHom.range_eq_map` `MonoidHom.range_eq_top` `MulEquiv.surjective` `Subgroup.map_commutator` `Subgroup.mem_map_of_mem`
`kleinFour_isKleinFour` 📖	mathematical	`Nat.card`	`IsKleinFour` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `kleinFour`	—	`kleinFour_card_of_card_eq_four` `exponent_kleinFour_of_card_eq_four`
`mem_kleinFour_of_order_two_pow` 📖	mathematical	`Nat.card` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Monoid.toNatPow` `Nat.instMonoid`	`Equiv.Perm.cycleType` `Multiset` `Multiset.instEmptyCollection` `Multiset.instInsert` `Multiset.instSingleton`	—	`Equiv.Perm.sum_cycleType` `Nat.card_eq_fintype_card` `Finset.card_le_univ` `LE.le.trans` `Multiset.le_sum_of_mem` `Nat.instCanonicallyOrderedAdd` `Equiv.Perm.one_lt_of_mem_cycleType` `Mathlib.Tactic.Contrapose.contrapose₁` `Multiset.exists_cons_of_mem` `Multiset.eq_replicate_card` `Multiset.sum_eq_zero_iff` `Nat.instIsOrderedAddMonoid` `le_zero_iff` `add_le_iff_nonpos_right` `IsOrderedAddMonoid.toAddLeftMono` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Multiset.sum_cons` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `Multiset.sum_singleton` `Multiset.card_singleton` `Equiv.Perm.sign_of_cycleType` `Equiv.Perm.mem_alternatingGroup` `le_antisymm` `Mathlib.Tactic.IntervalCases.of_le_right` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.prime_eq_prime_of_dvd_pow` `Nat.prime_three` `Nat.prime_two` `Multiset.lcm_dvd` `Equiv.Perm.lcm_cycleType` `Mathlib.Tactic.IntervalCases.of_lt_left` `two_pos` `Nat.instZeroLEOneClass` `smul_eq_mul` `Multiset.sum_replicate` `Mathlib.Meta.NormNum.isNat_natDiv`
`normal_kleinFour` 📖	mathematical	`Nat.card`	`Subgroup.Normal` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `kleinFour`	—	`characteristic_kleinFour` `Subgroup.normal_of_characteristic`
`subsingleton_two_sylow` 📖	mathematical	`Nat.card`	`Sylow` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup`	—	`Sylow.ext_iff` `two_sylow_eq_kleinFour_of_card_eq_four`
`two_sylow_eq_kleinFour_of_card_eq_four` 📖	mathematical	`Nat.card`	`Sylow.toSubgroup` `Equiv.Perm` `Subgroup` `Equiv.Perm.permGroup` `SetLike.instMembership` `Subgroup.instSetLike` `alternatingGroup` `Subgroup.toGroup` `kleinFour`	—	`kleinFour.eq_1` `Subgroup.closure_insert_one` `Set.singleton_union` `coe_two_sylow_of_card_eq_four` `Subgroup.closure_eq`

---

← Back to Index