Epi

📁 Source: Mathlib/Algebra/Category/Ring/Epi.lean

Statistics

Metric	Count
Definitions	0
Theorems epi_iff_epi, epi_iff_tmul_eq_tmul, surjective_iff_epi_and_finite, surjective_of_epi_of_finite	4
Total	4

CommRingCat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff_epi 📖	mathematical	—	CategoryTheory.Epi CommRingCat instCategory of ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Algebra.IsEpi	—	CategoryTheory.Epi.left_cancellation hom_ext RingHom.ext Algebra.algebraMap_eq_smul_one TensorProduct.smul_tmul TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.left RingHom.congr_fun IsScalarTower.to_smulCommClass Commute.all map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass mul_one one_mul
epi_iff_tmul_eq_tmul 📖	mathematical	—	CategoryTheory.Epi CommRingCat instCategory of ofHom algebraMap CommRing.toCommSemiring CommSemiring.toSemiring Algebra.IsEpi	—	epi_iff_epi

RingHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
surjective_iff_epi_and_finite 📖	mathematical	—	CommRingCat.carrier DFunLike.coe CategoryTheory.ConcreteCategory.hom CommRingCat CommRingCat.instCategory RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing instFunLike CommRingCat.instConcreteCategoryRingHomCarrier CategoryTheory.Epi Finite CommRingCat.Hom.hom	—	CategoryTheory.ConcreteCategory.epi_of_surjective Finite.of_surjective surjective_of_epi_of_finite
surjective_of_epi_of_finite 📖	mathematical	—	CommRingCat.carrier DFunLike.coe CategoryTheory.ConcreteCategory.hom CommRingCat CommRingCat.instCategory RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing instFunLike CommRingCat.instConcreteCategoryRingHomCarrier	—	CommRingCat.epi_iff_epi Algebra.isEpi_iff_surjective_algebraMap_of_finite

---

← Back to Index