Documentation Verification Report

Subrepresentation

📁 Source: FLT/Deformations/RepresentationTheory/Subrepresentation.lean

Statistics

Metric	Count
Definitions `Subrepresentation`, `instBoundedOrder`, `instLattice`, `instMax`, `instMin`, `instSetLike`, `toRepresentation`, `toSubmodule`	8
Theorems `apply_mem_toSubmodule`, `coe_inf`, `coe_sup`, `toSubmodule_inf`, `toSubmodule_injective`, `toSubmodule_sup`	6
Total	14

Subrepresentation

Definitions

Name	Category	Theorems
`instBoundedOrder` 📖	CompOp	1 math math: `Representation.IsIrreducible.irreducible`
`instLattice` 📖	CompOp	1 math math: `Representation.IsIrreducible.irreducible`
`instMax` 📖	CompOp	2 math math: `toSubmodule_sup`, `coe_sup`
`instMin` 📖	CompOp	2 math math: `toSubmodule_inf`, `coe_inf`
`instSetLike` 📖	CompOp	2 math math: `coe_inf`, `coe_sup`
`toRepresentation` 📖	CompOp	—
`toSubmodule` 📖	CompOp	3 math math: `toSubmodule_inf`, `toSubmodule_sup`, `toSubmodule_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_mem_toSubmodule` 📖	—	`toSubmodule`	—	—	—
`coe_inf` 📖	mathematical	—	`Subrepresentation` `instSetLike` `instMin`	—	—
`coe_sup` 📖	mathematical	—	`Subrepresentation` `instSetLike` `instMax`	—	—
`toSubmodule_inf` 📖	mathematical	—	`toSubmodule` `Subrepresentation` `instMin`	—	—
`toSubmodule_injective` 📖	mathematical	—	`Subrepresentation` `toSubmodule`	—	`apply_mem_toSubmodule`
`toSubmodule_sup` 📖	mathematical	—	`toSubmodule` `Subrepresentation` `instMax`	—	—

(root)

Definitions

Name	Category	Theorems
`Subrepresentation` 📖	CompData	6 math math: `Subrepresentation.toSubmodule_inf`, `Subrepresentation.toSubmodule_sup`, `Subrepresentation.toSubmodule_injective`, `Subrepresentation.coe_inf`, `Subrepresentation.coe_sup`, `Representation.IsIrreducible.irreducible`

---

← Back to Index