Ring

📁 Source: MathlibTest/CategoryTheory/ConcreteCategory/Ring.lean

Statistics

Metric	Count
Definitions Ring, Ring	2
Theorems	0
Total	2

StandardEtalePair

Definitions

Name	Category	Theorems
Ring 📖	CompOp	20 math math: inv_aeval_X_g, Algebra.instIsStandardEtaleRing, homEquiv_symm_apply, StandardEtalePresentation.toPresentation_algebra_smul, homEquiv_apply_coe, hasMap_X, equivMvPolynomialQuotient_symm_apply, instFormallyEtaleRing, lift_X, StandardEtalePresentation.equivRing_x, StandardEtalePresentation.lift_bijective, hom_ext_iff, StandardEtalePresentation.toPresentation_σ', aeval_X_g_mul_mk_X, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, StandardEtalePresentation.toPresentation_val, lift_X_left, StandardEtalePresentation.toPresentation_relation, instEtaleRing, StandardEtalePresentation.equivRing_symm_X

(root)

Definitions

Name	Category	Theorems
Ring 📖	CompData	5 math math: Ring.toSemiring_injective, Ring.toNonAssocRing_injective, CommRing.toRing_injective, Ring.toNonUnitalRing_injective, nonempty_ring_iff

---

← Back to Index