Documentation Verification Report

DMatrix

📁 Source: Mathlib/Data/Matrix/DMatrix.lean

Statistics

Metric	Count
Definitions `mapDMatrix`, `DMatrix`, `col`, `instAdd`, `instAddCommGroup`, `instAddCommMonoid`, `instAddCommSemigroup`, `instAddGroup`, `instAddMonoid`, `instAddSemigroup`, `instInhabited`, `instNeg`, `instSub`, `instUnique`, `instZero`, `map`, `row`, `transpose`, `«term_ᵀ»`	19
Theorems `mapDMatrix_apply`, `add_apply`, `ext`, `ext_iff`, `instSubsingleton`, `map_add`, `map_apply`, `map_map`, `map_sub`, `map_zero`, `neg_apply`, `sub_apply`, `subsingleton_of_empty_left`, `subsingleton_of_empty_right`, `zero_apply`	15
Total	34

AddMonoidHom

Definitions

Name	Category	Theorems
`mapDMatrix` 📖	CompOp	1 math math: `mapDMatrix_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapDMatrix_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `DMatrix` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DMatrix.instAddMonoid` `instFunLike` `mapDMatrix` `DMatrix.map`	—	—

DMatrix

Definitions

Name	Category	Theorems
`col` 📖	CompOp	—
`instAdd` 📖	CompOp	2 math math: `add_apply`, `map_add`
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	—
`instAddCommSemigroup` 📖	CompOp	—
`instAddGroup` 📖	CompOp	—
`instAddMonoid` 📖	CompOp	1 math math: `AddMonoidHom.mapDMatrix_apply`
`instAddSemigroup` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instNeg` 📖	CompOp	1 math math: `neg_apply`
`instSub` 📖	CompOp	2 math math: `sub_apply`, `map_sub`
`instUnique` 📖	CompOp	—
`instZero` 📖	CompOp	2 math math: `zero_apply`, `map_zero`
`map` 📖	CompOp	6 math math: `map_map`, `map_add`, `map_zero`, `AddMonoidHom.mapDMatrix_apply`, `map_apply`, `map_sub`
`row` 📖	CompOp	—
`transpose` 📖	CompOp	—
`«term_ᵀ»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DMatrix` `instAdd`	—	—
`ext` 📖	—	—	—	—	`ext_iff`
`ext_iff` 📖	—	—	—	—	—
`instSubsingleton` 📖	mathematical	—	`DMatrix`	—	—
`map_add` 📖	mathematical	—	`map` `DMatrix` `instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidHom.instFunLike`	—	`ext` `map_add` `AddMonoidHomClass.toAddHomClass` `AddMonoidHom.instAddMonoidHomClass`
`map_apply` 📖	mathematical	—	`map`	—	—
`map_map` 📖	mathematical	—	`map`	—	`ext`
`map_sub` 📖	mathematical	—	`map` `DMatrix` `instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddMonoidHom.instFunLike`	—	`ext` `map_sub` `AddMonoidHom.instAddMonoidHomClass`
`map_zero` 📖	mathematical	—	`map` `DMatrix` `instZero`	—	`ext`
`neg_apply` 📖	mathematical	—	`DMatrix` `instNeg`	—	—
`sub_apply` 📖	mathematical	—	`DMatrix` `instSub`	—	—
`subsingleton_of_empty_left` 📖	mathematical	—	`DMatrix`	—	`ext`
`subsingleton_of_empty_right` 📖	mathematical	—	`DMatrix`	—	`ext`
`zero_apply` 📖	mathematical	—	`DMatrix` `instZero`	—	—

(root)

Definitions

Name	Category	Theorems
`DMatrix` 📖	CompOp	11 math math: `DMatrix.add_apply`, `DMatrix.subsingleton_of_empty_left`, `DMatrix.neg_apply`, `DMatrix.instSubsingleton`, `DMatrix.map_add`, `DMatrix.subsingleton_of_empty_right`, `DMatrix.zero_apply`, `DMatrix.map_zero`, `AddMonoidHom.mapDMatrix_apply`, `DMatrix.sub_apply`, `DMatrix.map_sub`

---

← Back to Index