Documentation Verification Report

ModN

📁 Source: Mathlib/LinearAlgebra/FreeModule/ModN.lean

Statistics

Metric	Count
Definitions `ModN`, `basis`, `instModuleZMod`, `liftEquiv`, `liftEquiv'`, `mkQ`	6
Theorems `basis_apply_eq_mkQ`, `instFinite`, `instModuleFinite`, `natCard_eq`	4
Total	10

ModN

Definitions

Name	Category	Theorems
`basis` 📖	CompOp	1 math math: `basis_apply_eq_mkQ`
`instModuleZMod` 📖	CompOp	2 math math: `basis_apply_eq_mkQ`, `instModuleFinite`
`liftEquiv` 📖	CompOp	—
`liftEquiv'` 📖	CompOp	—
`mkQ` 📖	CompOp	1 math math: `basis_apply_eq_mkQ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basis_apply_eq_mkQ` 📖	mathematical	—	`DFunLike.coe` `Module.Basis` `ZMod` `ModN` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `AddCommGroup.toAddCommMonoid` `Submodule.Quotient.addCommGroup` `Int.instRing` `AddCommGroup.toIntModule` `LinearMap.range` `Int.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.addCommMonoid` `Semiring.toModule` `LinearMap.module` `LinearMap.instFunLike` `LinearMap.lsmul` `instModuleZMod` `Module.Basis.instFunLike` `basis` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `AddMonoidHom.instFunLike` `mkQ` `Int.instSemiring`	—	`RingHomInvPair.ids` `Module.Basis.apply_eq_iff` `Module.Basis.repr_self` `LinearMap.map_zero` `Finsupp.mapRange_single` `Int.cast_one`
`instFinite` 📖	mathematical	—	`Finite` `ModN`	—	`Module.finite_of_finite` `Finite.of_fintype` `instModuleFinite`
`instModuleFinite` 📖	mathematical	—	`Module.Finite` `ZMod` `ModN` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing` `AddCommGroup.toAddCommMonoid` `Submodule.Quotient.addCommGroup` `Int.instRing` `AddCommGroup.toIntModule` `LinearMap.range` `Int.instCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `DFunLike.coe` `LinearMap` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.addCommMonoid` `Semiring.toModule` `LinearMap.module` `LinearMap.instFunLike` `LinearMap.lsmul` `instModuleZMod`	—	`Module.Finite.of_basis` `Finite.of_fintype`
`natCard_eq` 📖	mathematical	—	`Nat.card` `ModN` `Monoid.toNatPow` `Nat.instMonoid` `Module.finrank` `Int.instSemiring` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toIntModule`	—	`Nat.card_congr` `RingHomInvPair.ids` `Nat.card_eq_fintype_card` `Fintype.card_finsupp` `ZMod.card` `Module.finrank_eq_card_chooseBasisIndex` `IsNoetherianRing.strongRankCondition` `Int.instNontrivial` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain`

(root)

Definitions

Name	Category	Theorems
`ModN` 📖	CompOp	4 math math: `ModN.basis_apply_eq_mkQ`, `ModN.natCard_eq`, `ModN.instFinite`, `ModN.instModuleFinite`

---

← Back to Index