Documentation Verification Report

TransferInstance

📁 Source: Mathlib/Algebra/Ring/TransferInstance.lean

Statistics

Metric	Count
Definitions `addGroupWithOne`, `addMonoidWithOne`, `commRing`, `commSemiring`, `nonAssocRing`, `nonAssocSemiring`, `nonUnitalCommRing`, `nonUnitalCommSemiring`, `nonUnitalNonAssocRing`, `nonUnitalNonAssocSemiring`, `nonUnitalRing`, `nonUnitalSemiring`, `ringEquiv`, `semiring`	14
Theorems `isDomain`, `ringEquiv_apply`, `ringEquiv_symm_apply`	3
Total	17

Equiv

Definitions

Name	Category	Theorems
`addGroupWithOne` 📖	CompOp	—
`addMonoidWithOne` 📖	CompOp	—
`commRing` 📖	CompOp	—
`commSemiring` 📖	CompOp	—
`nonAssocRing` 📖	CompOp	—
`nonAssocSemiring` 📖	CompOp	—
`nonUnitalCommRing` 📖	CompOp	—
`nonUnitalCommSemiring` 📖	CompOp	—
`nonUnitalNonAssocRing` 📖	CompOp	—
`nonUnitalNonAssocSemiring` 📖	CompOp	—
`nonUnitalRing` 📖	CompOp	—
`nonUnitalSemiring` 📖	CompOp	—
`ringEquiv` 📖	CompOp	2 math math: `ringEquiv_apply`, `ringEquiv_symm_apply`
`semiring` 📖	CompOp	4 math math: `algEquiv_apply`, `isDomain`, `algebraMap_def`, `algEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isDomain` 📖	mathematical	—	`IsDomain` `semiring`	—	`Function.Injective.isDomain` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `injective`
`ringEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `mul` `add` `ringEquiv` `Equiv` `instEquivLike`	—	—
`ringEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `mul` `add` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `ringEquiv` `Equiv` `instEquivLike` `symm`	—	—

---

← Back to Index