Documentation Verification Report

Synonym

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

Statistics

Metric	Count
Definitions `instAddCommMonoidWithOneLex`, `instAddCommMonoidWithOneOrderDual`, `instAddMonoidWithOneLex`, `instAddMonoidWithOneOrderDual`, `instNatCastLex`, `instNatCastOrderDual`	6
Theorems `ofDual_natCast`, `ofDual_ofNat`, `ofLex_natCast`, `ofLex_ofNat`, `toDual_natCast`, `toDual_ofNat`, `toLex_natCast`, `toLex_ofNat`	8
Total	14

(root)

Definitions

Name	Category	Theorems
`instAddCommMonoidWithOneLex` 📖	CompOp	—
`instAddCommMonoidWithOneOrderDual` 📖	CompOp	—
`instAddMonoidWithOneLex` 📖	CompOp	—
`instAddMonoidWithOneOrderDual` 📖	CompOp	—
`instNatCastLex` 📖	CompOp	3 math math: `toLex_ofNat`, `ofLex_natCast`, `toLex_natCast`
`instNatCastOrderDual` 📖	CompOp	2 math math: `ofDual_natCast`, `toDual_natCast`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ofDual_natCast` 📖	mathematical	—	`DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual` `instNatCastOrderDual`	—	—
`ofDual_ofNat` 📖	mathematical	—	`DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.ofDual`	—	—
`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`	—	—
`toDual_natCast` 📖	mathematical	—	`DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual` `instNatCastOrderDual`	—	—
`toDual_ofNat` 📖	mathematical	—	`DFunLike.coe` `Equiv` `OrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	—	—
`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