FreeCommRing

📁 Source: Mathlib/ModelTheory/Algebra/Ring/FreeCommRing.lean

Statistics

Metric	Count
Definitions termOfFreeCommRing	1
Theorems realize_termOfFreeCommRing	1
Total	2

FirstOrder.Ring

Definitions

Name	Category	Theorems
termOfFreeCommRing 📖	CompOp	1 math math: realize_termOfFreeCommRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
realize_termOfFreeCommRing 📖	mathematical	—	FirstOrder.Language.Term.realize FirstOrder.Language.ring CompatibleRing.toStructure Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass termOfFreeCommRing DFunLike.coe RingHom FreeCommRing Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRingFreeCommRing RingHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike FreeCommRing.lift	—	termOfFreeCommRing.eq_1 FreeCommRing.lift_of CompatibleRing.funMap_add map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass CompatibleRing.funMap_mul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass CompatibleRing.funMap_neg map_neg CompatibleRing.funMap_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass CompatibleRing.funMap_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass

---

← Back to Index