Documentation Verification Report

ZMod

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

Statistics

Metric	Count
Definitions `algebra`, `algebra'`, `algebraOfModule`	3
Theorems `proof`, `instIsScalarTower`, `instSubsingletonAlgebra`	3
Total	6

ZMod

Definitions

Name	Category	Theorems
`algebra` 📖	CompOp	1 math math: `FiniteField.instIsScalarTowerZModExtension`
`algebra'` 📖	CompOp	—
`algebraOfModule` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `ZMod` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`Algebra.smul_def` `SemigroupAction.mul_smul` `instSubsingletonModule`
`instSubsingletonAlgebra` 📖	mathematical	—	`Algebra` `ZMod` `CommRing.toCommSemiring` `commRing` `Ring.toSemiring`	—	`Algebra.algebra_ext` `RingHom.congr_fun` `subsingleton_ringHom`

ZMod.algebraOfModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`proof` 📖	mathematical	—	`Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `ZMod` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidWithOne.toOne`	—	—

---

← Back to Index