Documentation Verification Report

Rat

📁 Source: Mathlib/Algebra/Algebra/Hom/Rat.lean

Statistics

Metric	Count
Definitions `equivRatAlgHom`, `toRatAlgHom`	2
Theorems `toRingHom_toRatAlgHom`, `equivRatAlgHom_apply`, `equivRatAlgHom_symm_apply`, `toRatAlgHom_apply`, `toRatAlgHom_toRingHom`	5
Total	7

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toRingHom_toRatAlgHom` 📖	mathematical	—	`RingHom.toRatAlgHom` `RingHomClass.toRingHom` `AlgHom` `Rat.commSemiring` `Ring.toSemiring` `funLike` `Semiring.toNonAssocSemiring` `AlgHomClass.toRingHomClass` `algHomClass`	—	`ext` `AlgHomClass.toRingHomClass` `algHomClass`

RingHom

Definitions

Name	Category	Theorems
`equivRatAlgHom` 📖	CompOp	3 math math: `NumberField.basisMatrix_eq_embeddingsMatrixReindex`, `equivRatAlgHom_apply`, `equivRatAlgHom_symm_apply`
`toRatAlgHom` 📖	CompOp	4 math math: `AlgHom.toRingHom_toRatAlgHom`, `toRatAlgHom_apply`, `toRatAlgHom_toRingHom`, `equivRatAlgHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`equivRatAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `AlgHom` `Rat.commSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `equivRatAlgHom` `toRatAlgHom`	—	—
`equivRatAlgHom_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AlgHom` `Rat.commSemiring` `Ring.toSemiring` `RingHom` `Semiring.toNonAssocSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `equivRatAlgHom` `AlgHom.toRingHom`	—	—
`toRatAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Rat.commSemiring` `Ring.toSemiring` `AlgHom.funLike` `toRatAlgHom` `RingHom` `Semiring.toNonAssocSemiring` `instFunLike`	—	—
`toRatAlgHom_toRingHom` 📖	mathematical	—	`RingHomClass.toRingHom` `AlgHom` `Rat.commSemiring` `Ring.toSemiring` `AlgHom.funLike` `Semiring.toNonAssocSemiring` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `toRatAlgHom`	—	`ext` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`

---

← Back to Index