PGroup

📁 Source: Mathlib/GroupTheory/PGroup.lean

Statistics

Metric	Count
Definitions `IsPGroup`, `commGroupOfCardEqPrimeSq`, `powEquiv`, `powEquiv'`	4
Theorems `bot_lt_center`, `card_center_eq_prime_pow`, `card_eq_or_dvd`, `card_modEq_card_fixedPoints`, `card_orbit`, `center_nontrivial`, `comap_of_injective`, `comap_of_ker_isPGroup`, `comap_subtype`, `commutative_of_card_eq_prime_sq`, `coprime_card_of_ne`, `cyclic_center_quotient_of_card_eq_prime_sq`, `disjoint_of_ne`, `exists_card_eq`, `exists_fixed_point_of_prime_dvd_card_of_fixed_point`, `iff_card`, `iff_orderOf`, `index`, `ker_isPGroup_of_injective`, `le_or_disjoint_of_coprime`, `map`, `nonempty_fixed_point_of_prime_not_dvd_card`, `nontrivial_iff_card`, `of_bot`, `of_card`, `of_equiv`, `of_injective`, `of_surjective`, `orderOf_coprime`, `powEquiv_apply`, `powEquiv_symm_apply`, `to_inf_left`, `to_inf_right`, `to_le`, `to_quotient`, `to_subgroup`, `to_sup_of_normal_left`, `to_sup_of_normal_left'`, `to_sup_of_normal_right`, `to_sup_of_normal_right'`, `isPGroup_multiplicative`	41
Total	45

IsPGroup

Definitions

Name	Category	Theorems
`commGroupOfCardEqPrimeSq` 📖	CompOp	—
`powEquiv` 📖	CompOp	2 math math: `powEquiv_apply`, `powEquiv_symm_apply`
`powEquiv'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_lt_center` 📖	mathematical	`IsPGroup`	`Subgroup` `Preorder.toLT` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Bot.bot` `Subgroup.instBot` `Subgroup.center`	—	`bot_lt_iff_ne_bot` `Subgroup.one_lt_card_iff_ne_bot` `Subgroup.instFiniteSubtypeMem` `Finite.one_lt_card` `center_nontrivial`
`card_center_eq_prime_pow` 📖	mathematical	`Nat.card` `Monoid.toNatPow` `Nat.instMonoid`	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.center`	—	`Nat.finite_of_card_ne_zero` `pow_ne_zero` `isReduced_of_noZeroDivisors` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `NeZero.of_gt'` `Nat.Prime.one_lt'` `to_subgroup` `of_card` `nontrivial_iff_card` `Subgroup.instFiniteSubtypeMem` `center_nontrivial`
`card_eq_or_dvd` 📖	mathematical	`IsPGroup`	`Nat.card`	—	`finite_or_infinite` `iff_card` `pow_succ'` `Nat.card_eq_zero_of_infinite`
`card_modEq_card_fixedPoints` 📖	mathematical	`IsPGroup`	`Nat.ModEq` `Nat.card` `Set.Elem` `MulAction.fixedPoints` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Subtype.finite` `Nat.card_eq_fintype_card` `Fintype.card_congr` `Fintype.card_sigma` `ZMod.natCast_eq_natCast_iff` `Nat.cast_sum` `Fintype.card_congr'` `Finset.sum_bij_ne_zero` `Finset.mem_univ` `MulAction.mem_fixedPoints'` `Quotient.exact'` `Quotient.inductionOn'` `card_orbit` `Mathlib.Tactic.Contrapose.contrapose₂` `Nat.cast_pow` `CharP.cast_eq_zero` `ZMod.charP` `zero_pow` `MulAction.mem_fixedPoints_iff_card_orbit_eq_one` `pow_zero` `ne_of_eq_of_ne` `Nat.cast_one` `one_ne_zero` `NeZero.one` `ZMod.nontrivial` `Nat.Prime.one_lt'` `Finset.sum_const` `mul_one`
`card_orbit` 📖	mathematical	`IsPGroup`	`Nat.card` `Set.Elem` `MulAction.orbit` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `Monoid.toNatPow` `Nat.instMonoid`	—	`Nat.card_congr` `index` `Subgroup.finiteIndex_of_finite_quotient` `Finite.of_equiv`
`center_nontrivial` 📖	mathematical	`IsPGroup`	`Nontrivial` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.center`	—	`exists_fixed_point_of_prime_dvd_card_of_fixed_point` `of_equiv` `nontrivial_iff_card` `dvd_pow_self` `ne_of_gt` `ConjAct.fixedPoints_eq_center` `Subgroup.one_mem`
`comap_of_injective` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`Subgroup.comap`	—	`comap_of_ker_isPGroup` `ker_isPGroup_of_injective`
`comap_of_ker_isPGroup` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `MonoidHom.ker` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`Subgroup.comap`	—	`MonoidHom.map_pow` `Subgroup.coe_pow` `pow_add` `pow_mul`
`comap_subtype` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	`Subgroup.comap` `Subgroup.subtype`	—	`comap_of_injective` `Subtype.coe_injective`
`commutative_of_card_eq_prime_sq` 📖	mathematical	`Nat.card` `Monoid.toNatPow` `Nat.instMonoid`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`CommGroup.mul_comm`
`coprime_card_of_ne` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	`Nat.card`	—	`iff_card` `Nat.coprime_pow_primes` `Fact.elim`
`cyclic_center_quotient_of_card_eq_prime_sq` 📖	mathematical	`Nat.card` `Monoid.toNatPow` `Nat.instMonoid`	`IsCyclic` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `Subgroup.center` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `QuotientGroup.Quotient.group` `Subgroup.instNormalCenter`	—	`isCyclic_of_card_dvd_prime` `Subgroup.instNormalCenter` `mul_dvd_mul_iff_left` `IsCancelMulZero.toIsLeftCancelMulZero` `Nat.instIsCancelMulZero` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `sq` `Subgroup.card_mul_index` `mul_dvd_mul_right` `card_center_eq_prime_pow` `zero_lt_two` `Nat.instZeroLEOneClass` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `dvd_pow_self` `LT.lt.ne'`
`disjoint_of_ne` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	`Disjoint` `Subgroup.instPartialOrder` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice`	—	`Subgroup.disjoint_def` `iff_orderOf` `pow_zero` `eq_of_prime_pow_eq` `Nat.instIsCancelMulZero` `Unique.instSubsingleton` `Nat.Prime.prime` `Fact.out`
`exists_card_eq` 📖	mathematical	`IsPGroup`	`Nat.card` `Monoid.toNatPow` `Nat.instMonoid`	—	`iff_card`
`exists_fixed_point_of_prime_dvd_card_of_fixed_point` 📖	—	`IsPGroup` `Nat.card` `Set` `Set.instMembership` `MulAction.fixedPoints` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—	`Nat.modEq_zero_iff_dvd` `Nat.ModEq.trans` `Nat.ModEq.symm` `card_modEq_card_fixedPoints` `Dvd.dvd.modEq_zero_nat` `LT.lt.trans_le` `Nat.Prime.one_lt` `Fact.out` `Finite.card_pos_iff` `Subtype.finite` `exists_ne` `Finite.one_lt_card_iff_nontrivial`
`iff_card` 📖	mathematical	—	`IsPGroup` `Nat.card` `Monoid.toNatPow` `Nat.instMonoid`	—	`LT.lt.ne'` `Nat.card_pos` `One.instNonempty` `Nat.mem_primeFactorsList` `exists_prime_orderOf_dvd_card'` `iff_orderOf` `Nat.Prime.pow_eq_iff` `List.prod_replicate` `Nat.prod_primeFactorsList` `of_card`
`iff_orderOf` 📖	mathematical	—	`IsPGroup` `orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Monoid.toNatPow` `Nat.instMonoid`	—	`Nat.dvd_prime_pow` `Fact.out` `orderOf_dvd_of_pow_eq_one` `pow_orderOf_eq_one`
`index` 📖	mathematical	`IsPGroup`	`Subgroup.index` `Monoid.toNatPow` `Nat.instMonoid`	—	`Subgroup.normalCore_normal` `iff_card` `Subgroup.finite_quotient_of_finiteIndex` `Subgroup.finiteIndex_normalCore` `to_quotient` `Nat.dvd_prime_pow` `Fact.out` `Subgroup.index_eq_card` `Subgroup.index_dvd_of_le` `Subgroup.normalCore_le`
`ker_isPGroup_of_injective` 📖	mathematical	`DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `MonoidHom.ker` `Subgroup.toGroup`	—	`MonoidHom.ker_eq_bot_iff` `of_bot`
`le_or_disjoint_of_coprime` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Nat.card` `Subgroup.index`	`Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Disjoint` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Subgroup.instCompleteLattice`	—	`Subgroup.index_eq_one` `le_top` `Subgroup.card_eq_one` `disjoint_bot_left` `Nat.finite_of_card_ne_zero` `Subgroup.card_mul_index` `mul_ne_zero` `IsStrictOrderedRing.noZeroDivisors` `Nat.instIsStrictOrderedRing` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `exists_card_eq` `Subgroup.instFiniteSubtypeMem` `Nat.Prime.coprime_pow_of_not_dvd` `Fact.out` `Mathlib.Tactic.Contrapose.contrapose₁` `Nat.Prime.not_coprime_iff_dvd` `Subgroup.relIndex_eq_one` `Nat.eq_one_of_dvd_coprimes` `Subgroup.relIndex_dvd_index_of_normal` `Subgroup.relIndex_dvd_card` `disjoint_iff` `Subgroup.inf_eq_bot_of_coprime`
`map` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	`Subgroup.map`	—	`Subgroup.range_subtype` `MonoidHom.map_range` `of_surjective` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `MonoidHom.rangeRestrict_surjective`
`nonempty_fixed_point_of_prime_not_dvd_card` 📖	mathematical	`IsPGroup` `Nat.card`	`Set.Nonempty` `MulAction.fixedPoints` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Nat.finite_of_card_ne_zero` `dvd_zero` `Set.Nonempty.of_subtype` `Finite.card_pos_iff` `Subtype.finite` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `Mathlib.Tactic.Contrapose.contrapose₄` `Nat.modEq_zero_iff_dvd` `card_modEq_card_fixedPoints`
`nontrivial_iff_card` 📖	mathematical	`IsPGroup`	`Nontrivial` `Nat.card` `Monoid.toNatPow` `Nat.instMonoid`	—	`iff_card` `LT.lt.ne'` `Finite.one_lt_card` `pow_zero` `Finite.one_lt_card_iff_nontrivial` `one_lt_pow₀` `Nat.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.Prime.one_lt` `Fact.out` `ne_of_gt`
`of_bot` 📖	mathematical	—	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Bot.bot` `Subgroup.instBot` `Subgroup.toGroup`	—	`of_card` `Subgroup.card_bot` `pow_zero`
`of_card` 📖	mathematical	`Nat.card` `Monoid.toNatPow` `Nat.instMonoid`	`IsPGroup`	—	`pow_card_eq_one'`
`of_equiv` 📖	—	`IsPGroup`	—	—	`of_surjective` `MulEquiv.surjective`
`of_injective` 📖	—	`IsPGroup` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	—	—	`MonoidHom.map_pow` `MonoidHom.map_one`
`of_surjective` 📖	—	`IsPGroup` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MonoidHom.instFunLike`	—	—	`MonoidHom.map_pow` `MonoidHom.map_one`
`orderOf_coprime` 📖	mathematical	`IsPGroup`	`orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`orderOf_dvd_of_pow_eq_one`
`powEquiv_apply` 📖	mathematical	`IsPGroup`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `powEquiv` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`powEquiv_symm_apply` 📖	mathematical	`IsPGroup`	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `powEquiv` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `Nat.gcdB` `orderOf` `DivInvMonoid.toMonoid`	—	`Nat.card_zpowers`
`to_inf_left` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	`Subgroup.instMin`	—	`to_le` `inf_le_left`
`to_inf_right` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	`Subgroup.instMin`	—	`to_le` `inf_le_right`
`to_le` 📖	—	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder`	—	—	`of_injective`
`to_quotient` 📖	mathematical	`IsPGroup`	`HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `QuotientGroup.Quotient.group`	—	`of_surjective` `Quotient.mk''_surjective`
`to_subgroup` 📖	mathematical	`IsPGroup`	`Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	—	`of_injective` `Subtype.coe_injective`
`to_sup_of_normal_left` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Subgroup.instCompleteLattice`	—	`to_sup_of_normal_right` `sup_comm`
`to_sup_of_normal_left'` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.normalizer`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Subgroup.instCompleteLattice`	—	`to_sup_of_normal_right'` `sup_comm`
`to_sup_of_normal_right` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Subgroup.instCompleteLattice`	—	`QuotientGroup.ker_mk'` `Subgroup.comap_map_eq` `comap_of_ker_isPGroup` `map`
`to_sup_of_normal_right'` 📖	mathematical	`IsPGroup` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.toGroup` `Preorder.toLE` `PartialOrder.toPreorder` `Subgroup.instPartialOrder` `Subgroup.normalizer`	`SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Subgroup.instCompleteLattice`	—	`to_sup_of_normal_right` `of_equiv` `Subgroup.le_normalizer` `Subgroup.normal_in_normalizer` `Subgroup.subgroupOf_sup` `sup_le`

ZModModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPGroup_multiplicative` 📖	mathematical	—	`IsPGroup` `Multiplicative` `Multiplicative.group` `AddCommGroup.toAddGroup`	—	`pow_one` `char_nsmul_eq_zero`

(root)

Definitions

Name	Category	Theorems
`IsPGroup` 📖	MathDef	8 math math: `Sylow.isPGroup'`, `IsPGroup.iff_card`, `ZModModule.isPGroup_multiplicative`, `IsPGroup.ker_isPGroup_of_injective`, `IsPGroup.of_bot`, `CommGroup.primaryComponent.isPGroup`, `IsPGroup.iff_orderOf`, `IsPGroup.of_card`

---

← Back to Index