Documentation Verification Report

TransferInstance

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

Statistics

Metric	Count
Definitions `algEquiv`, `algebra`	2
Theorems `algEquiv_apply`, `algEquiv_symm_apply`, `algebraMap_def`	3
Total	5

Equiv

Definitions

Name	Category	Theorems
`algEquiv` 📖	CompOp	2 math math: `algEquiv_apply`, `algEquiv_symm_apply`
`algebra` 📖	CompOp	3 math math: `algEquiv_apply`, `algebraMap_def`, `algEquiv_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv.instFunLike` `semiring` `algebra` `algEquiv` `Equiv` `EquivLike.toFunLike` `instEquivLike`	—	—
`algEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `semiring` `algebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `algEquiv` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—
`algebraMap_def` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `semiring` `RingHom.instFunLike` `algebraMap` `algebra` `Equiv` `EquivLike.toFunLike` `instEquivLike` `symm`	—	—

---

← Back to Index