Documentation Verification Report

Basic

📁 Source: Mathlib/Analysis/Normed/Order/Hom/Basic.lean

Statistics

Metric	Count
Definitions `toNormedAddCommGroup`, `toNormedAddGroup`, `toSeminormedAddCommGroup`, `toSeminormedAddGroup`, `toNormedCommGroup`, `toNormedGroup`, `toSeminormedCommGroup`, `toSeminormedGroup`	8
Theorems `toNormedAddCommGroup_norm_eq`, `toNormedAddGroup_norm_eq`, `toSeminormedAddCommGroup_norm_eq`, `toSeminormedAddGroup_norm_eq`, `toNormedCommGroup_norm_eq`, `toNormedGroup_norm_eq`, `toSeminormedCommGroup_norm_eq`, `toSeminormedGroup_norm_eq`	8
Total	16

AddGroupNormClass

Definitions

Name	Category	Theorems
`toNormedAddCommGroup` 📖	CompOp	1 math math: `toNormedAddCommGroup_norm_eq`
`toNormedAddGroup` 📖	CompOp	1 math math: `toNormedAddGroup_norm_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toNormedAddCommGroup_norm_eq` 📖	mathematical	—	`Norm.norm` `NormedAddCommGroup.toNorm` `toNormedAddCommGroup` `DFunLike.coe` `Real`	—	—
`toNormedAddGroup_norm_eq` 📖	mathematical	—	`Norm.norm` `NormedAddGroup.toNorm` `toNormedAddGroup` `DFunLike.coe` `Real`	—	—

AddGroupSeminormClass

Definitions

Name	Category	Theorems
`toSeminormedAddCommGroup` 📖	CompOp	1 math math: `toSeminormedAddCommGroup_norm_eq`
`toSeminormedAddGroup` 📖	CompOp	1 math math: `toSeminormedAddGroup_norm_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toSeminormedAddCommGroup_norm_eq` 📖	mathematical	—	`Norm.norm` `SeminormedAddCommGroup.toNorm` `toSeminormedAddCommGroup` `DFunLike.coe` `Real`	—	—
`toSeminormedAddGroup_norm_eq` 📖	mathematical	—	`Norm.norm` `SeminormedAddGroup.toNorm` `toSeminormedAddGroup` `DFunLike.coe` `Real`	—	—

GroupNormClass

Definitions

Name	Category	Theorems
`toNormedCommGroup` 📖	CompOp	1 math math: `toNormedCommGroup_norm_eq`
`toNormedGroup` 📖	CompOp	1 math math: `toNormedGroup_norm_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toNormedCommGroup_norm_eq` 📖	mathematical	—	`Norm.norm` `NormedCommGroup.toNorm` `toNormedCommGroup` `DFunLike.coe` `Real`	—	—
`toNormedGroup_norm_eq` 📖	mathematical	—	`Norm.norm` `NormedGroup.toNorm` `toNormedGroup` `DFunLike.coe` `Real`	—	—

GroupSeminormClass

Definitions

Name	Category	Theorems
`toSeminormedCommGroup` 📖	CompOp	1 math math: `toSeminormedCommGroup_norm_eq`
`toSeminormedGroup` 📖	CompOp	1 math math: `toSeminormedGroup_norm_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toSeminormedCommGroup_norm_eq` 📖	mathematical	—	`Norm.norm` `SeminormedCommGroup.toNorm` `toSeminormedCommGroup` `DFunLike.coe` `Real`	—	—
`toSeminormedGroup_norm_eq` 📖	mathematical	—	`Norm.norm` `SeminormedGroup.toNorm` `toSeminormedGroup` `DFunLike.coe` `Real`	—	—

---

← Back to Index