Documentation Verification Report

Opposite

📁 Source: Mathlib/Algebra/Field/Opposite.lean

Statistics

Metric	Count
Definitions `instDivisionRing`, `instDivisionSemiring`, `instField`, `instNNRatCast`, `instRatCast`, `instSemifield`, `instDivisionRing`, `instDivisionSemiring`, `instField`, `instNNRatCast`, `instRatCast`, `instSemifield`	12
Theorems `op_nnratCast`, `op_ratCast`, `unop_nnratCast`, `unop_ratCast`, `op_nnratCast`, `op_ratCast`, `unop_nnratCast`, `unop_ratCast`	8
Total	20

AddOpposite

Definitions

Name	Category	Theorems
`instDivisionRing` 📖	CompOp	—
`instDivisionSemiring` 📖	CompOp	—
`instField` 📖	CompOp	—
`instNNRatCast` 📖	CompOp	2 math math: `unop_nnratCast`, `op_nnratCast`
`instRatCast` 📖	CompOp	2 math math: `unop_ratCast`, `op_ratCast`
`instSemifield` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`op_nnratCast` 📖	mathematical	—	`op` `NNRat.cast` `AddOpposite` `instNNRatCast`	—	—
`op_ratCast` 📖	mathematical	—	`op` `AddOpposite` `instRatCast`	—	—
`unop_nnratCast` 📖	mathematical	—	`unop` `NNRat.cast` `AddOpposite` `instNNRatCast`	—	—
`unop_ratCast` 📖	mathematical	—	`unop` `AddOpposite` `instRatCast`	—	—

MulOpposite

Definitions

Name	Category	Theorems
`instDivisionRing` 📖	CompOp	—
`instDivisionSemiring` 📖	CompOp	—
`instField` 📖	CompOp	—
`instNNRatCast` 📖	CompOp	2 math math: `unop_nnratCast`, `op_nnratCast`
`instRatCast` 📖	CompOp	2 math math: `op_ratCast`, `unop_ratCast`
`instSemifield` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`op_nnratCast` 📖	mathematical	—	`op` `NNRat.cast` `MulOpposite` `instNNRatCast`	—	—
`op_ratCast` 📖	mathematical	—	`op` `MulOpposite` `instRatCast`	—	—
`unop_nnratCast` 📖	mathematical	—	`unop` `NNRat.cast` `MulOpposite` `instNNRatCast`	—	—
`unop_ratCast` 📖	mathematical	—	`unop` `MulOpposite` `instRatCast`	—	—

---

← Back to Index