Singleton

📁 Source: Mathlib/RingTheory/Adjoin/Singleton.lean

Statistics

Metric	Count
Definitions adjoinAlgebraMap, adjoinAlgebraMapEquiv, instSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap	3
Theorems adjoin_algebraMap_apply, adjoin_algebraMap_surjective, instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap	3
Total	6

Algebra

Definitions

Name	Category	Theorems
instSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap 📖	CompOp	1 math math: instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsScalarTowerSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap 📖	mathematical	—	IsScalarTower Subalgebra CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike adjoin Set Set.instSingletonSet DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap toSMul Polynomial.instCommSemiringAdjoinSingleton Subalgebra.toSemiring instSubtypeMemSubalgebraAdjoinSingletonSetCoeRingHomAlgebraMap Subalgebra.instSMulSubtypeMem id	—	IsScalarTower.of_algebraMap_eq'

Algebra.RingHom

Definitions

Name	Category	Theorems
adjoinAlgebraMap 📖	CompOp	2 math math: adjoin_algebraMap_apply, adjoin_algebraMap_surjective
adjoinAlgebraMapEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_algebraMap_apply 📖	mathematical	—	Subalgebra CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Subalgebra.toSemiring adjoinAlgebraMap	—	—
adjoin_algebraMap_surjective 📖	mathematical	—	Subalgebra CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Subalgebra.toSemiring adjoinAlgebraMap	—	Algebra.adjoin_eq_exists_aeval Polynomial.aeval_algebraMap_apply

---

← Back to Index