Documentation Verification Report

Equiv

📁 Source: Mathlib/Algebra/Order/Group/Equiv.lean

Statistics

Metric	Count
Definitions `ofLexAddEquiv`, `ofLexMulEquiv`, `toLexAddEquiv`, `toLexMulEquiv`	4
Theorems `coe_ofLexAddEquiv`, `coe_ofLexMulEquiv`, `coe_toLexAddEquiv`, `coe_toLexMulEquiv`, `symm_ofLexAddEquiv`, `symm_ofLexMulEquiv`, `symm_toLexAddEquiv`, `symm_toLexMulEquiv`, `toEquiv_ofLexAddEquiv`, `toEquiv_ofLexMulEquiv`, `toEquiv_toLexAddEquiv`, `toEquiv_toLexMulEquiv`	12
Total	16

(root)

Definitions

Name	Category	Theorems
`ofLexAddEquiv` 📖	CompOp	4 math math: `symm_ofLexAddEquiv`, `symm_toLexAddEquiv`, `coe_ofLexAddEquiv`, `toEquiv_ofLexAddEquiv`
`ofLexMulEquiv` 📖	CompOp	5 math math: `coe_ofLexMulEquiv`, `symm_ofLexMulEquiv`, `toEquiv_ofLexMulEquiv`, `LinearOrderedCommGroupWithZero.fst_apply`, `symm_toLexMulEquiv`
`toLexAddEquiv` 📖	CompOp	4 math math: `symm_ofLexAddEquiv`, `symm_toLexAddEquiv`, `toEquiv_toLexAddEquiv`, `coe_toLexAddEquiv`
`toLexMulEquiv` 📖	CompOp	6 math math: `toEquiv_toLexMulEquiv`, `symm_ofLexMulEquiv`, `coe_toLexMulEquiv`, `symm_toLexMulEquiv`, `LinearOrderedCommGroupWithZero.inl_apply`, `LinearOrderedCommGroupWithZero.inr_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_ofLexAddEquiv` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Lex` `instAddLex` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `ofLexAddEquiv` `Equiv` `Equiv.instEquivLike` `ofLex`	—	—
`coe_ofLexMulEquiv` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Lex` `instMulLex` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `ofLexMulEquiv` `Equiv` `Equiv.instEquivLike` `ofLex`	—	—
`coe_toLexAddEquiv` 📖	mathematical	—	`DFunLike.coe` `AddEquiv` `Lex` `instAddLex` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `toLexAddEquiv` `Equiv` `Equiv.instEquivLike` `toLex`	—	—
`coe_toLexMulEquiv` 📖	mathematical	—	`DFunLike.coe` `MulEquiv` `Lex` `instMulLex` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `toLexMulEquiv` `Equiv` `Equiv.instEquivLike` `toLex`	—	—
`symm_ofLexAddEquiv` 📖	mathematical	—	`AddEquiv.symm` `Lex` `instAddLex` `ofLexAddEquiv` `toLexAddEquiv`	—	—
`symm_ofLexMulEquiv` 📖	mathematical	—	`MulEquiv.symm` `Lex` `instMulLex` `ofLexMulEquiv` `toLexMulEquiv`	—	—
`symm_toLexAddEquiv` 📖	mathematical	—	`AddEquiv.symm` `Lex` `instAddLex` `toLexAddEquiv` `ofLexAddEquiv`	—	—
`symm_toLexMulEquiv` 📖	mathematical	—	`MulEquiv.symm` `Lex` `instMulLex` `toLexMulEquiv` `ofLexMulEquiv`	—	—
`toEquiv_ofLexAddEquiv` 📖	mathematical	—	`EquivLike.toEquiv` `Lex` `AddEquiv` `instAddLex` `AddEquiv.instEquivLike` `ofLexAddEquiv` `ofLex`	—	—
`toEquiv_ofLexMulEquiv` 📖	mathematical	—	`EquivLike.toEquiv` `Lex` `MulEquiv` `instMulLex` `MulEquiv.instEquivLike` `ofLexMulEquiv` `ofLex`	—	—
`toEquiv_toLexAddEquiv` 📖	mathematical	—	`EquivLike.toEquiv` `Lex` `AddEquiv` `instAddLex` `AddEquiv.instEquivLike` `toLexAddEquiv` `toLex`	—	—
`toEquiv_toLexMulEquiv` 📖	mathematical	—	`EquivLike.toEquiv` `Lex` `MulEquiv` `instMulLex` `MulEquiv.instEquivLike` `toLexMulEquiv` `toLex`	—	—

---

← Back to Index