Documentation Verification Report

RingInvo

📁 Source: Mathlib/RingTheory/RingInvo.lean

Statistics

Metric	Count
Definitions `RingInvo`, `id`, `instCoeTCOfRingInvoClass`, `instEquivLikeMulOpposite`, `mk'`, `toRingEquiv`, `RingInvoClass`, `toRingInvo`, `instInhabitedRingInvo`	9
Theorems `coe_ringEquiv`, `instRingInvoClass`, `involution`, `involution'`, `map_eq_zero_iff`, `involution`, `toRingEquivClass`	7
Total	16

RingInvo

Definitions

Name	Category	Theorems
`id` 📖	CompOp	—
`instCoeTCOfRingInvoClass` 📖	CompOp	—
`instEquivLikeMulOpposite` 📖	CompOp	4 math math: `instRingInvoClass`, `involution`, `coe_ringEquiv`, `map_eq_zero_iff`
`mk'` 📖	CompOp	—
`toRingEquiv` 📖	CompOp	1 math math: `involution'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_ringEquiv` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `MulOpposite` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulOpposite.instMul` `Distrib.toAdd` `MulOpposite.instAdd` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquivClass.toRingEquiv` `RingInvo` `instEquivLikeMulOpposite` `RingInvoClass.toRingEquivClass` `instRingInvoClass`	—	`RingInvoClass.toRingEquivClass` `instRingInvoClass`
`instRingInvoClass` 📖	mathematical	—	`RingInvoClass` `RingInvo` `instEquivLikeMulOpposite`	—	`RingEquiv.map_mul'` `RingEquiv.map_add'` `involution'`
`involution` 📖	mathematical	—	`MulOpposite.unop` `DFunLike.coe` `RingInvo` `MulOpposite` `EquivLike.toFunLike` `instEquivLikeMulOpposite`	—	`involution'`
`involution'` 📖	mathematical	—	`MulOpposite.unop` `Equiv.toFun` `MulOpposite` `RingEquiv.toEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `MulOpposite.instMul` `Distrib.toAdd` `MulOpposite.instAdd` `toRingEquiv`	—	—
`map_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `RingInvo` `MulOpposite` `EquivLike.toFunLike` `instEquivLikeMulOpposite` `MulOpposite.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`RingEquiv.map_eq_zero_iff`

RingInvoClass

Definitions

Name	Category	Theorems
`toRingInvo` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`involution` 📖	mathematical	—	`MulOpposite.unop` `DFunLike.coe` `MulOpposite` `EquivLike.toFunLike`	—	—
`toRingEquivClass` 📖	mathematical	—	`RingEquivClass` `MulOpposite` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `MulOpposite.instMul` `MulOpposite.instAdd`	—	—

(root)

Definitions

Name	Category	Theorems
`RingInvo` 📖	CompData	4 math math: `RingInvo.instRingInvoClass`, `RingInvo.involution`, `RingInvo.coe_ringEquiv`, `RingInvo.map_eq_zero_iff`
`RingInvoClass` 📖	CompData	1 math math: `RingInvo.instRingInvoClass`
`instInhabitedRingInvo` 📖	CompOp	—

---

← Back to Index