ZMod

📁 Source: Mathlib/Algebra/Module/ZMod.lean

Statistics

Metric	Count
Definitions zmodModule, zmodModule, toZModLinearMap, toZModLinearMapEquiv, toZModSubmodule, zmodModule	6
Theorems coe_toZModLinearMap, toZModLinearMap_injective, coe_toZModSubmodule, mem_toZModSubmodule, toZModSubmodule_symm, toZModSubmodule_toAddSubgroup, toAddSubgroup_toZModSubmodule, map_smul, smul_mem, exists_submodule_subset_card_le	10
Total	16

AddCommGroup

Definitions

Name	Category	Theorems
zmodModule 📖	CompOp	—

AddCommMonoid

Definitions

Name	Category	Theorems
zmodModule 📖	CompOp	—

AddMonoidHom

Definitions

Name	Category	Theorems
toZModLinearMap 📖	CompOp	2 math math: toZModLinearMap_injective, coe_toZModLinearMap
toZModLinearMapEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toZModLinearMap 📖	mathematical	—	DFunLike.coe LinearMap ZMod CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike toZModLinearMap AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instFunLike	—	—
toZModLinearMap_injective 📖	mathematical	—	AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup LinearMap ZMod CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid toZModLinearMap	—	ext

AddSubgroup

Definitions

Name	Category	Theorems
toZModSubmodule 📖	CompOp	5 math math: Submodule.toAddSubgroup_toZModSubmodule, toZModSubmodule_toAddSubgroup, toZModSubmodule_symm, coe_toZModSubmodule, mem_toZModSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toZModSubmodule 📖	mathematical	—	SetLike.coe Submodule ZMod CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing AddCommGroup.toAddCommMonoid Submodule.setLike DFunLike.coe OrderIso AddSubgroup AddCommGroup.toAddGroup Preorder.toLE PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder instFunLikeOrderIso toZModSubmodule instSetLike	—	—
mem_toZModSubmodule 📖	mathematical	—	Submodule ZMod CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike DFunLike.coe OrderIso AddSubgroup AddCommGroup.toAddGroup Preorder.toLE PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder instFunLikeOrderIso toZModSubmodule instSetLike	—	—
toZModSubmodule_symm 📖	mathematical	—	DFunLike.coe OrderIso Submodule ZMod CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing AddCommGroup.toAddCommMonoid AddSubgroup AddCommGroup.toAddGroup Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder instPartialOrder instFunLikeOrderIso OrderIso.symm toZModSubmodule Submodule.toAddSubgroup CommRing.toRing	—	—
toZModSubmodule_toAddSubgroup 📖	mathematical	—	Submodule.toAddSubgroup ZMod CommRing.toRing ZMod.commRing DFunLike.coe OrderIso AddSubgroup AddCommGroup.toAddGroup Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder Submodule.instPartialOrder instFunLikeOrderIso toZModSubmodule	—	—

QuotientAddGroup

Definitions

Name	Category	Theorems
zmodModule 📖	CompOp	—

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toAddSubgroup_toZModSubmodule 📖	mathematical	—	DFunLike.coe OrderIso AddSubgroup AddCommGroup.toAddGroup Submodule ZMod CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder instPartialOrder instFunLikeOrderIso AddSubgroup.toZModSubmodule toAddSubgroup CommRing.toRing	—	—

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_smul 📖	mathematical	—	DFunLike.coe ZMod SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring commRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	intCast_zmod_cast map_intCast_smul
smul_mem 📖	mathematical	SetLike.instMembership	ZMod SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring commRing Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	intCast_zmod_cast Int.cast_smul_eq_zsmul zsmul_mem

ZModModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_submodule_subset_card_le 📖	mathematical	Nat.Prime Nat.card Submodule ZMod CommSemiring.toSemiring CommRing.toCommSemiring ZMod.commRing AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike	Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder	—	Sylow.exists_subgroup_le_card_le isPGroup_multiplicative

---

← Back to Index