RingHom

📁 Source: Mathlib/Algebra/Module/RingHom.lean

Statistics

Metric	Count
Definitions moduleLeft, compHom, smulOneHom, toModule, ringHomEquivModuleIsScalarTower	5
Theorems smulOneHom_apply	1
Total	6

Function.Surjective

Definitions

Name	Category	Theorems
moduleLeft 📖	CompOp	—

Module

Definitions

Name	Category	Theorems
compHom 📖	CompOp	16 math math: PresheafOfModules.restrictScalarsObj_map, ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.toRestrictScalars_hom_apply, ModuleCat.RestrictionCoextensionAdj.counit'_app, ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars_hom_apply, ModuleCat.ExtendScalars.smul_tmul, ModuleCat.ExtendScalars.map_tmul, compHom.toLinearMap_apply, MatrixModCat.isScalarTower_toModuleCat, ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.evalAt_apply, ModuleCat.extendScalarsComp_hom_app_one_tmul, Basis.mapCoeffs_repr, ModuleCat.extendRestrictScalarsAdj_unit_app_apply, PresheafOfModules.ofPresheaf_map, compHom.toLinearEquiv_symm_apply, ModuleCat.semilinearMapAddEquiv_apply, compHom.toLinearEquiv_apply

RingHom

Definitions

Name	Category	Theorems
smulOneHom 📖	CompOp	3 math math: smulOneHom_eq_algebraMap, smulOneHom_apply, Polynomial.eval₂_smulOneHom_eq_smeval
toModule 📖	CompOp	3 math math: Subalgebra.inclusion.isScalarTower_left, Subalgebra.inclusion.isScalarTower_right, Subalgebra.inclusion.faithfulSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smulOneHom_apply 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring instFunLike smulOneHom SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Module.toDistribMulAction MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass	—	—

(root)

Definitions

Name	Category	Theorems
ringHomEquivModuleIsScalarTower 📖	CompOp	—

---

← Back to Index