Documentation Verification Report

Synonym

📁 Source: Mathlib/Data/Nat/Cast/Synonym.lean

Statistics

Metric	Count
Definitions `instAddCommMonoidWithOneLex`, `instAddMonoidWithOneLex`, `instNatCastLex`	3
Theorems `ofLex_natCast`, `ofLex_ofNat`, `toLex_natCast`, `toLex_ofNat`	4
Total	7

(root)

Definitions

Name	Category	Theorems
`instAddCommMonoidWithOneLex` 📖	CompOp	—
`instAddMonoidWithOneLex` 📖	CompOp	—
`instNatCastLex` 📖	CompOp	3 math math: `toLex_ofNat`, `ofLex_natCast`, `toLex_natCast`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofLex_natCast` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `instNatCastLex`	—	—
`ofLex_ofNat` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `ofLex` `instOfNatAtLeastTwo`	—	—
`toLex_natCast` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `instNatCastLex`	—	—
`toLex_ofNat` 📖	mathematical	—	`DFunLike.coe` `Equiv` `Lex` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex` `instOfNatAtLeastTwo` `instNatCastLex`	—	—

---

← Back to Index