Documentation Verification Report

Hom

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

Statistics

Metric	Count
Definitions `Hom`, `SemialgHom`, `toLinearMap`, `toRingHom`, `SemialgHomClass`, `instFunLike`, `«term_→ₛₐ[_]_»`, `«term_→ₛₐ_»`	8
Theorems `algebraMap_apply`, `commutes`, `map_mul'`, `map_one'`, `map_smul`, `map_zero'`, `toLinearMap_eq_coe`, `toRingHom_eq_coe`, `instSemialgHom`, `toMonoidHomClass`, `toRingHomClass`, `toSemilinearMapClass`, `toZeroHomClass`, `coe_mk`	14
Total	22

Deformation.ProartinianCat

Definitions

Name	Category	Theorems
`Hom` 📖	CompData	—

SemialgHom

Definitions

Name	Category	Theorems
`toLinearMap` 📖	CompOp	4 math math: `map_zero'`, `map_mul'`, `map_one'`, `toLinearMap_eq_coe`
`toRingHom` 📖	CompOp	4 math math: `baseChangeRightOfAlgebraMap_coe`, `baseChangeRightOfAlgebraMap_apply`, `toRingHom_eq_coe`, `algebraMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_apply` 📖	mathematical	—	`toRingHom` `SemialgHom` `instFunLike`	—	—
`commutes` 📖	mathematical	—	`SemialgHom` `instFunLike`	—	`map_smul` `SemialgHomClass.toRingHomClass` `SemialgHomClass.instSemialgHom`
`map_mul'` 📖	mathematical	—	`toLinearMap`	—	—
`map_one'` 📖	mathematical	—	`toLinearMap`	—	—
`map_smul` 📖	mathematical	—	`SemialgHom` `instFunLike`	—	—
`map_zero'` 📖	mathematical	—	`toLinearMap`	—	—
`toLinearMap_eq_coe` 📖	mathematical	—	`toLinearMap` `SemialgHom` `instFunLike` `SemialgHomClass.toSemilinearMapClass` `SemialgHomClass.instSemialgHom`	—	—
`toRingHom_eq_coe` 📖	mathematical	—	`toRingHom` `SemialgHom` `instFunLike` `SemialgHomClass.toRingHomClass` `SemialgHomClass.instSemialgHom`	—	—

SemialgHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instSemialgHom` 📖	mathematical	—	`SemialgHomClass` `SemialgHom` `instFunLike`	—	—
`toMonoidHomClass` 📖	—	—	—	—	—
`toRingHomClass` 📖	—	—	—	—	`toMonoidHomClass` `toSemilinearMapClass` `toZeroHomClass`
`toSemilinearMapClass` 📖	—	—	—	—	—
`toZeroHomClass` 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
`SemialgHom` 📖	CompData	30 math math: `SemialgHom.baseChange_of_algebraMap_tmul_right`, `SemialgHom.map_smul`, `IsDedekindDomain.cofinite_mapsTo_adicCompletionComapSemialgHom`, `Pi.semialgHom_apply`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom.mapadicCompletionIntegers`, `Pi.semialgHomPi_apply`, `NumberField.InfinitePlace.Completion.piEquiv_smul`, `SemialgHom.commutes`, `UniformSpace.Completion.mapSemialgHom_coe`, `AbsoluteValue.Completion.semiAlgHomOfComp_dist_eq`, `SemialgHom.toRingHom_eq_coe`, `IsDedekindDomain.FiniteAdeleRing.mapSemialgHom_continuous`, `NumberField.InfinitePlace.Completion.baseChangeEquiv_tmul`, `UniformSpace.Completion.mapSemialgHom_apply`, `SemialgHom.algebraMap_apply`, `NumberField.InfinitePlace.Completion.comapHom_cont`, `NumberField.InfiniteAdeleRing.baseChange_cont`, `IsDedekindDomain.HeightOneSpectrum.valued_adicCompletionComap`, `NumberField.InfiniteAdeleRing.baseChangeEquivAux_tmul`, `SemialgHom.toLinearMap_eq_coe`, `IsDedekindDomain.HeightOneSpectrum.comap_integer_algebraMap`, `AbsoluteValue.Completion.isometry_semiAlgHomOfComp`, `SemialgHomClass.instSemialgHom`, `NumberField.InfinitePlace.Completion.piExtension_apply`, `IsDedekindDomain.FiniteAdeleRing.mapSemialgHom_apply`, `SemialgHom.baseChange_of_algebraMap_tmul`, `coe_mk`, `AbsoluteValue.Completion.semialgHomOfComp_coe`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom_continuous`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionComap_coe`
`SemialgHomClass` 📖	CompData	1 math math: `SemialgHomClass.instSemialgHom`
`instFunLike` 📖	CompOp	30 math math: `SemialgHom.baseChange_of_algebraMap_tmul_right`, `SemialgHom.map_smul`, `IsDedekindDomain.cofinite_mapsTo_adicCompletionComapSemialgHom`, `Pi.semialgHom_apply`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom.mapadicCompletionIntegers`, `Pi.semialgHomPi_apply`, `NumberField.InfinitePlace.Completion.piEquiv_smul`, `SemialgHom.commutes`, `UniformSpace.Completion.mapSemialgHom_coe`, `AbsoluteValue.Completion.semiAlgHomOfComp_dist_eq`, `SemialgHom.toRingHom_eq_coe`, `IsDedekindDomain.FiniteAdeleRing.mapSemialgHom_continuous`, `NumberField.InfinitePlace.Completion.baseChangeEquiv_tmul`, `UniformSpace.Completion.mapSemialgHom_apply`, `SemialgHom.algebraMap_apply`, `NumberField.InfinitePlace.Completion.comapHom_cont`, `NumberField.InfiniteAdeleRing.baseChange_cont`, `IsDedekindDomain.HeightOneSpectrum.valued_adicCompletionComap`, `NumberField.InfiniteAdeleRing.baseChangeEquivAux_tmul`, `SemialgHom.toLinearMap_eq_coe`, `IsDedekindDomain.HeightOneSpectrum.comap_integer_algebraMap`, `AbsoluteValue.Completion.isometry_semiAlgHomOfComp`, `SemialgHomClass.instSemialgHom`, `NumberField.InfinitePlace.Completion.piExtension_apply`, `IsDedekindDomain.FiniteAdeleRing.mapSemialgHom_apply`, `SemialgHom.baseChange_of_algebraMap_tmul`, `coe_mk`, `AbsoluteValue.Completion.semialgHomOfComp_coe`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionComapSemialgHom_continuous`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionComap_coe`
`«term_→ₛₐ[_]_»` 📖	CompOp	—
`«term_→ₛₐ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_mk` 📖	mathematical	—	`SemialgHom` `instFunLike`	—	—

---

← Back to Index