Documentation Verification Report

QuotientGroup

📁 Source: Mathlib/Data/ZMod/QuotientGroup.lean

Statistics

Metric	Count
Definitions `orbitZMultiplesEquiv`, `zmultiplesQuotientStabilizerEquiv`, `quotientZMultiplesEquivZMod`, `quotientZMultiplesNatEquivZMod`, `orbitZPowersEquiv`, `zpowersQuotientStabilizerEquiv`, `quotientEquivSigmaZMod`	7
Theorems `minimalPeriod_eq_card`, `minimalPeriod_pos`, `orbitZMultiplesEquiv_symm_apply`, `orbitZMultiplesEquiv_symm_apply'`, `zmultiplesQuotientStabilizerEquiv_symm_apply`, `index_zmultiples`, `finite_zmultiples`, `finite_zpowers`, `minimalPeriod_eq_card`, `minimalPeriod_pos`, `orbitZPowersEquiv_symm_apply`, `orbitZPowersEquiv_symm_apply'`, `zpowersQuotientStabilizerEquiv_symm_apply`, `card_zmultiples`, `card_zpowers`, `quotientEquivSigmaZMod_apply`, `quotientEquivSigmaZMod_symm_apply`, `finite_zmultiples`, `finite_zpowers`, `infinite_zmultiples`, `infinite_zpowers`	21
Total	28

AddAction

Definitions

Name	Category	Theorems
`orbitZMultiplesEquiv` 📖	CompOp	2 math math: `orbitZMultiplesEquiv_symm_apply'`, `orbitZMultiplesEquiv_symm_apply`
`zmultiplesQuotientStabilizerEquiv` 📖	CompOp	1 math math: `zmultiplesQuotientStabilizerEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`minimalPeriod_eq_card` 📖	mathematical	—	`Function.minimalPeriod` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `Fintype.card` `Set.Elem` `orbit` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples` `AddSubgroup.toAddGroup` `instAddAction`	—	`Fintype.ofEquiv_card` `ZMod.card`
`minimalPeriod_pos` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `Function.minimalPeriod` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction`	—	`nonempty_fintype` `minimalPeriod_eq_card` `Fintype.card_ne_zero` `Set.Nonempty.to_subtype` `nonempty_orbit`
`orbitZMultiplesEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ZMod` `Function.minimalPeriod` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `Set.Elem` `orbit` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples` `AddSubgroup.toAddGroup` `instAddAction` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `orbitZMultiplesEquiv` `instElemOrbit` `AddSubgroup.zsmul` `ZMod.cast` `Ring.toAddGroupWithOne` `Int.instRing` `AddSubgroup.mem_zmultiples` `Set` `Set.instMembership` `mem_orbit_self`	—	—
`orbitZMultiplesEquiv_symm_apply'` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ZMod` `Function.minimalPeriod` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `Set.Elem` `orbit` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples` `AddSubgroup.toAddGroup` `instAddAction` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `orbitZMultiplesEquiv` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `instElemOrbit` `AddSubgroup.zsmul` `AddSubgroup.mem_zmultiples` `Set` `Set.instMembership` `mem_orbit_self`	—	`AddSubgroup.mem_zmultiples` `mem_orbit_self` `orbitZMultiplesEquiv_symm_apply` `ZMod.coe_intCast` `zsmul_vadd_mod_minimalPeriod`
`zmultiplesQuotientStabilizerEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `ZMod` `Function.minimalPeriod` `HVAdd.hVAdd` `instHVAdd` `AddSemigroupAction.toVAdd` `AddMonoid.toAddSemigroup` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `toAddSemigroupAction` `HasQuotient.Quotient` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples` `AddSubgroup.toAddGroup` `QuotientAddGroup.instHasQuotientAddSubgroup` `stabilizer` `instAddAction` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `QuotientAddGroup.Quotient.addCommGroup` `AddCommGroup.ofIsAddCommutative` `AddSubgroup.zmultiples_isAddCommutative` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `zmultiplesQuotientStabilizerEquiv` `SubNegMonoid.toZSMul` `QuotientAddGroup.Quotient.addGroup` `AddSubgroup.normal_of_comm` `ZMod.cast` `Ring.toAddGroupWithOne` `Int.instRing` `AddSubgroup.mem_zmultiples`	—	`AddSubgroup.zmultiples_isAddCommutative`

Int

Definitions

Name	Category	Theorems
`quotientZMultiplesEquivZMod` 📖	CompOp	—
`quotientZMultiplesNatEquivZMod` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`index_zmultiples` 📖	mathematical	—	`AddSubgroup.index` `instAddGroup` `AddSubgroup.zmultiples`	—	`AddSubgroup.index.eq_1` `Nat.card_congr` `Nat.card_zmod`

IsOfFinAddOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_zmultiples` 📖	mathematical	`IsOfFinAddOrder` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`Set.Finite` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples`	—	`finite_zmultiples`

IsOfFinOrder

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_zpowers` 📖	mathematical	`IsOfFinOrder` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`Set.Finite` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `Subgroup.zpowers`	—	`finite_zpowers`

MulAction

Definitions

Name	Category	Theorems
`orbitZPowersEquiv` 📖	CompOp	2 math math: `orbitZPowersEquiv_symm_apply`, `orbitZPowersEquiv_symm_apply'`
`zpowersQuotientStabilizerEquiv` 📖	CompOp	1 math math: `zpowersQuotientStabilizerEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`minimalPeriod_eq_card` 📖	mathematical	—	`Function.minimalPeriod` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `Fintype.card` `Set.Elem` `orbit` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `instMulAction`	—	`Fintype.ofEquiv_card` `ZMod.card`
`minimalPeriod_pos` 📖	mathematical	—	`MulZeroClass.toZero` `Nat.instMulZeroClass` `Function.minimalPeriod` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction`	—	`nonempty_fintype` `minimalPeriod_eq_card` `Fintype.card_ne_zero` `Set.Nonempty.to_subtype` `nonempty_orbit`
`orbitZPowersEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ZMod` `Function.minimalPeriod` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `Set.Elem` `orbit` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `instMulAction` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `orbitZPowersEquiv` `instElemOrbit` `Subgroup.zpow` `Subgroup.mem_zpowers` `ZMod.cast` `Ring.toAddGroupWithOne` `Int.instRing` `Set` `Set.instMembership` `mem_orbit_self`	—	—
`orbitZPowersEquiv_symm_apply'` 📖	mathematical	—	`DFunLike.coe` `Equiv` `ZMod` `Function.minimalPeriod` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `Set.Elem` `orbit` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `instMulAction` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `orbitZPowersEquiv` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing` `instElemOrbit` `Subgroup.zpow` `Subgroup.mem_zpowers` `Set` `Set.instMembership` `mem_orbit_self`	—	`Subgroup.mem_zpowers` `mem_orbit_self` `orbitZPowersEquiv_symm_apply` `ZMod.coe_intCast` `zpow_smul_mod_minimalPeriod`
`zpowersQuotientStabilizerEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Multiplicative` `ZMod` `Function.minimalPeriod` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `toSemigroupAction` `HasQuotient.Quotient` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `Subgroup.toGroup` `QuotientGroup.instHasQuotientSubgroup` `stabilizer` `instMulAction` `Multiplicative.mul` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `ZMod.commRing` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `QuotientGroup.Quotient.group` `Subgroup.normal_of_comm` `CommGroup.ofIsMulCommutative` `Subgroup.zpowers_isMulCommutative` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `zpowersQuotientStabilizerEquiv` `DivInvMonoid.toZPow` `Subgroup.mem_zpowers` `ZMod.cast` `Ring.toAddGroupWithOne` `Int.instRing`	—	`Subgroup.normal_of_comm` `Subgroup.zpowers_isMulCommutative`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_zmultiples` 📖	mathematical	—	`card` `AddSubgroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples` `addOrderOf` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`card_congr` `orbit_addSubgroup_zero_eq_self` `card_zmod`
`card_zpowers` 📖	mathematical	—	`card` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.zpowers` `orderOf` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`card_congr` `orbit_subgroup_one_eq_self` `card_zmod`

Subgroup

Definitions

Name	Category	Theorems
`quotientEquivSigmaZMod` 📖	CompOp	3 math math: `quotientEquivSigmaZMod_apply`, `transferFunction_apply`, `quotientEquivSigmaZMod_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`quotientEquivSigmaZMod_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `HasQuotient.Quotient` `Subgroup` `QuotientGroup.instHasQuotientSubgroup` `MulAction.orbitRel.Quotient` `SetLike.instMembership` `instSetLike` `zpowers` `toGroup` `MulAction.mulLeftCosetsCompSubtypeVal` `ZMod` `Function.minimalPeriod` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MulAction.quotient` `Monoid.toMulAction` `MulAction.left_quotientAction` `Quotient.out` `MulAction.orbitRel` `EquivLike.toFunLike` `Equiv.instEquivLike` `quotientEquivSigmaZMod` `DivInvMonoid.toZPow` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `CommRing.toRing` `ZMod.commRing`	—	`MulAction.left_quotientAction` `Equiv.apply_eq_iff_eq_symm_apply` `quotientEquivSigmaZMod_symm_apply` `ZMod.coe_intCast` `MulAction.zpow_smul_mod_minimalPeriod`
`quotientEquivSigmaZMod_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `MulAction.orbitRel.Quotient` `Subgroup` `SetLike.instMembership` `instSetLike` `zpowers` `HasQuotient.Quotient` `QuotientGroup.instHasQuotientSubgroup` `toGroup` `MulAction.mulLeftCosetsCompSubtypeVal` `ZMod` `Function.minimalPeriod` `SemigroupAction.toSMul` `Monoid.toSemigroup` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `MulAction.toSemigroupAction` `MulAction.quotient` `Monoid.toMulAction` `MulAction.left_quotientAction` `Quotient.out` `MulAction.orbitRel` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `quotientEquivSigmaZMod` `DivInvMonoid.toZPow` `ZMod.cast` `Ring.toAddGroupWithOne` `Int.instRing`	—	`MulAction.left_quotientAction`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_zmultiples` 📖	mathematical	—	`Set.Finite` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples` `IsOfFinAddOrder` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`addOrderOf_pos_iff` `Nat.card_zmultiples` `Nat.card_pos_iff` `Set.nonempty_coe_sort` `AddSubgroup.coe_nonempty` `Set.finite_coe_iff`
`finite_zpowers` 📖	mathematical	—	`Set.Finite` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `Subgroup.zpowers` `IsOfFinOrder` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`infinite_zmultiples` 📖	mathematical	—	`Set.Infinite` `SetLike.coe` `AddSubgroup` `AddSubgroup.instSetLike` `AddSubgroup.zmultiples` `IsOfFinAddOrder` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`Iff.not` `finite_zmultiples`
`infinite_zpowers` 📖	mathematical	—	`Set.Infinite` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `Subgroup.zpowers` `IsOfFinOrder` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Iff.not` `finite_zpowers`

---

← Back to Index