Documentation Verification Report

Comap

📁 Source: Mathlib/Algebra/MvPolynomial/Comap.lean

Statistics

Metric	Count
Definitions `comap`, `comapEquiv`	2
Theorems `comapEquiv_coe`, `comapEquiv_symm_coe`, `comap_apply`, `comap_comp`, `comap_comp_apply`, `comap_eq_id_of_eq_id`, `comap_id`, `comap_id_apply`, `comap_rename`	9
Total	11

MvPolynomial

Definitions

Name	Category	Theorems
`comap` 📖	CompOp	9 math math: `comapEquiv_symm_coe`, `comapEquiv_coe`, `comap_id`, `comap_comp_apply`, `comap_comp`, `comap_rename`, `comap_apply`, `comap_id_apply`, `comap_eq_id_of_eq_id`
`comapEquiv` 📖	CompOp	2 math math: `comapEquiv_symm_coe`, `comapEquiv_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comapEquiv_coe` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `comapEquiv` `comap` `AlgHomClass.toAlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgEquiv` `AlgEquiv.instFunLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass`	—	—
`comapEquiv_symm_coe` 📖	mathematical	—	`DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `comapEquiv` `comap` `AlgHomClass.toAlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgEquiv` `AlgEquiv.instFunLike` `AlgEquivClass.toAlgHomClass` `AlgEquiv.instEquivLike` `AlgEquiv.instAlgEquivClass` `AlgEquiv.symm`	—	—
`comap_apply` 📖	mathematical	—	`comap` `DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike` `aeval` `X`	—	—
`comap_comp` 📖	mathematical	—	`comap` `AlgHom.comp` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id`	—	`comap_comp_apply`
`comap_comp_apply` 📖	mathematical	—	`comap` `AlgHom.comp` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id`	—	`eval₂Hom_congr` `AlgHom.comp_apply` `aeval_unique` `map_eval₂Hom` `RingHom.ext` `aeval_C`
`comap_eq_id_of_eq_id` 📖	mathematical	`DFunLike.coe` `AlgHom` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id` `AlgHom.funLike`	`comap`	—	`algHom_ext` `comap_id_apply`
`comap_id` 📖	mathematical	—	`comap` `AlgHom.id` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id`	—	`comap_id_apply`
`comap_id_apply` 📖	mathematical	—	`comap` `AlgHom.id` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `algebra` `Algebra.id`	—	`aeval_X`
`comap_rename` 📖	mathematical	—	`comap` `rename`	—	`rename_X` `aeval_X`

---

← Back to Index