Documentation Verification Report

Subrepresentation

📁 Source: Mathlib/RepresentationTheory/Subrepresentation.lean

Statistics

Metric	Count
Definitions `Subrepresentation`, `asSubmodule`, `asSubmodule'`, `instBoundedOrder`, `instLattice`, `instMax`, `instMin`, `instPartialOrder`, `instSetLike`, `ofSubmodule`, `ofSubmodule'`, `submoduleSubrepresentationOrderIso`, `subrepresentationSubmoduleOrderIso`, `toRepresentation`, `toSubmodule`	15
Theorems `apply_mem_toSubmodule`, `coe_inf`, `coe_sup`, `mem_asSubmodule'_iff`, `mem_asSubmodule_iff`, `mem_ofSubmodule'_iff`, `mem_ofSubmodule_iff`, `submoduleSubrepresentationOrderIso_apply`, `submoduleSubrepresentationOrderIso_symm_apply`, `subrepresentationSubmoduleOrderIso_apply`, `subrepresentationSubmoduleOrderIso_symm_apply`, `toSubmodule_inf`, `toSubmodule_injective`, `toSubmodule_sup`	14
Total	29

Subrepresentation

Definitions

Name	Category	Theorems
`asSubmodule` 📖	CompOp	2 math math: `mem_asSubmodule_iff`, `subrepresentationSubmoduleOrderIso_apply`
`asSubmodule'` 📖	CompOp	2 math math: `mem_asSubmodule'_iff`, `submoduleSubrepresentationOrderIso_symm_apply`
`instBoundedOrder` 📖	CompOp	—
`instLattice` 📖	CompOp	—
`instMax` 📖	CompOp	2 math math: `toSubmodule_sup`, `coe_sup`
`instMin` 📖	CompOp	2 math math: `toSubmodule_inf`, `coe_inf`
`instPartialOrder` 📖	CompOp	4 math math: `submoduleSubrepresentationOrderIso_apply`, `subrepresentationSubmoduleOrderIso_symm_apply`, `subrepresentationSubmoduleOrderIso_apply`, `submoduleSubrepresentationOrderIso_symm_apply`
`instSetLike` 📖	CompOp	6 math math: `mem_ofSubmodule'_iff`, `mem_asSubmodule'_iff`, `mem_asSubmodule_iff`, `coe_inf`, `coe_sup`, `mem_ofSubmodule_iff`
`ofSubmodule` 📖	CompOp	2 math math: `submoduleSubrepresentationOrderIso_apply`, `mem_ofSubmodule_iff`
`ofSubmodule'` 📖	CompOp	2 math math: `mem_ofSubmodule'_iff`, `subrepresentationSubmoduleOrderIso_symm_apply`
`submoduleSubrepresentationOrderIso` 📖	CompOp	2 math math: `submoduleSubrepresentationOrderIso_apply`, `submoduleSubrepresentationOrderIso_symm_apply`
`subrepresentationSubmoduleOrderIso` 📖	CompOp	2 math math: `subrepresentationSubmoduleOrderIso_symm_apply`, `subrepresentationSubmoduleOrderIso_apply`
`toRepresentation` 📖	CompOp	—
`toSubmodule` 📖	CompOp	3 math math: `toSubmodule_inf`, `toSubmodule_sup`, `toSubmodule_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_mem_toSubmodule` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SetLike.instMembership` `Submodule.setLike` `toSubmodule`	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `Representation` `MonoidHom.instFunLike` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring`	—	—
`coe_inf` 📖	mathematical	—	`SetLike.coe` `Subrepresentation` `instSetLike` `instMin` `Set` `Set.instInter`	—	—
`coe_sup` 📖	mathematical	—	`SetLike.coe` `Subrepresentation` `instSetLike` `instMax` `Set` `Set.add` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	`Submodule.coe_sup`
`mem_asSubmodule'_iff` 📖	mathematical	—	`Submodule` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidAlgebra.semiring` `SetLike.instMembership` `Submodule.setLike` `asSubmodule'` `Subrepresentation` `RestrictScalars` `instAddCommMonoidRestrictScalars` `RestrictScalars.module` `MonoidAlgebra.algebra` `Algebra.id` `Representation.ofModule` `instSetLike`	—	—
`mem_asSubmodule_iff` 📖	mathematical	—	`Submodule` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Representation.asModule` `MonoidAlgebra.semiring` `Representation.instAddCommMonoidAsModule` `Representation.instModuleMonoidAlgebraAsModule` `SetLike.instMembership` `Submodule.setLike` `asSubmodule` `Subrepresentation` `instSetLike`	—	—
`mem_ofSubmodule'_iff` 📖	mathematical	—	`Subrepresentation` `SetLike.instMembership` `instSetLike` `ofSubmodule'` `Submodule` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Representation.asModule` `MonoidAlgebra.semiring` `Representation.instAddCommMonoidAsModule` `Representation.instModuleMonoidAlgebraAsModule` `Submodule.setLike`	—	—
`mem_ofSubmodule_iff` 📖	mathematical	—	`Subrepresentation` `RestrictScalars` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instAddCommMonoidRestrictScalars` `RestrictScalars.module` `MonoidAlgebra.semiring` `MonoidAlgebra.algebra` `Algebra.id` `Representation.ofModule` `SetLike.instMembership` `instSetLike` `ofSubmodule` `Submodule` `Submodule.setLike`	—	—
`submoduleSubrepresentationOrderIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Submodule` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `MonoidAlgebra.semiring` `Subrepresentation` `RestrictScalars` `instAddCommMonoidRestrictScalars` `RestrictScalars.module` `MonoidAlgebra.algebra` `Algebra.id` `Representation.ofModule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `instPartialOrder` `RelIso.instFunLike` `submoduleSubrepresentationOrderIso` `ofSubmodule`	—	—
`submoduleSubrepresentationOrderIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subrepresentation` `RestrictScalars` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instAddCommMonoidRestrictScalars` `RestrictScalars.module` `MonoidAlgebra.semiring` `MonoidAlgebra.algebra` `Algebra.id` `Representation.ofModule` `Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `submoduleSubrepresentationOrderIso` `asSubmodule'`	—	—
`subrepresentationSubmoduleOrderIso_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Subrepresentation` `Submodule` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Representation.asModule` `MonoidAlgebra.semiring` `Representation.instAddCommMonoidAsModule` `Representation.instModuleMonoidAlgebraAsModule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Submodule.instPartialOrder` `RelIso.instFunLike` `subrepresentationSubmoduleOrderIso` `asSubmodule`	—	—
`subrepresentationSubmoduleOrderIso_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RelIso` `Submodule` `MonoidAlgebra` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Representation.asModule` `MonoidAlgebra.semiring` `Representation.instAddCommMonoidAsModule` `Representation.instModuleMonoidAlgebraAsModule` `Subrepresentation` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `instPartialOrder` `RelIso.instFunLike` `RelIso.symm` `subrepresentationSubmoduleOrderIso` `ofSubmodule'`	—	—
`toSubmodule_inf` 📖	mathematical	—	`toSubmodule` `Subrepresentation` `instMin` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instMin`	—	—
`toSubmodule_injective` 📖	mathematical	—	`Subrepresentation` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `toSubmodule`	—	`apply_mem_toSubmodule`
`toSubmodule_sup` 📖	mathematical	—	`toSubmodule` `Subrepresentation` `instMax` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	—

(root)

Definitions

Name	Category	Theorems
`Subrepresentation` 📖	CompData	13 math math: `Subrepresentation.mem_ofSubmodule'_iff`, `Subrepresentation.toSubmodule_inf`, `Subrepresentation.toSubmodule_sup`, `Subrepresentation.toSubmodule_injective`, `Subrepresentation.mem_asSubmodule'_iff`, `Subrepresentation.submoduleSubrepresentationOrderIso_apply`, `Subrepresentation.mem_asSubmodule_iff`, `Subrepresentation.coe_inf`, `Subrepresentation.subrepresentationSubmoduleOrderIso_symm_apply`, `Subrepresentation.coe_sup`, `Subrepresentation.mem_ofSubmodule_iff`, `Subrepresentation.subrepresentationSubmoduleOrderIso_apply`, `Subrepresentation.submoduleSubrepresentationOrderIso_symm_apply`

---

← Back to Index