Structures · Logic and sets
FirstOrder.Ring.CompatibleRing
A Type R is a CompatibleRing if it is a structure for the language of rings and this
structure is the same as the structure already given on R by the classes Add, Mul etc.
It is recommended to use this type class as a hypothesis to any theorem whose statement
requires a type to have be both a Ring (or Field etc.) and a
Language.ring.Structure
- Defined in
- Mathlib.ModelTheory.Algebra.Ring.Basic
- Shape
- One type argument · adds funMap_add, funMap_mul, funMap_neg, funMap_zero, funMap_one
Extends1
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by27
- FirstOrder.Ring.realize_zero
- FirstOrder.Ring.realize_termOfFreeCommRing
- FirstOrder.Ring.CompatibleRing.funMap_mul
- FirstOrder.Field.charP_of_model_fieldOfChar
- FirstOrder.Ring.CompatibleRing.funMap_add
- FirstOrder.Field.isAlgClosed_of_model_ACF
- FirstOrder.Ring.CompatibleRing.funMap_one
- FirstOrder.Ring.CompatibleRing.funMap_neg
- FirstOrder.realize_genericPolyMapSurjOnOfInjOn
- FirstOrder.Ring.CompatibleRing.funMap_zero
- FirstOrder.Ring.languageEquivEquivRingEquiv
- FirstOrder.Field.realize_genericMonicPolyHasRoot
- FirstOrder.Field.FieldAxiom.realize_toSentence_iff_toProp
- FirstOrder.Ring.realize_mul
- FirstOrder.Ring.realize_neg
- FirstOrder.Ring.realize_add
- ax_grothendieck_of_definable
- FirstOrder.Ring.mvPolynomial_zeroLocus_definable
- FirstOrder.Field.charP_iff_model_fieldOfChar
- FirstOrder.Ring.realize_one
- FirstOrder.Field.instModelACFOfCharPOfIsAlgClosed
- FirstOrder.Ring.CompatibleRing.toStructure
- FirstOrder.Field.model_hasChar_of_charP
- FirstOrder.Field.FieldAxiom.toProp_of_model
- FirstOrder.Field.model_fieldOfChar_of_charP
- FirstOrder.Field.realize_eqZero
- FirstOrder.Field.instModelField