Theorems · Inductive type · logic and foundations
FirstOrder.Ring.CompatibleRing
(R : Type u_2) → [Add R] → [Mul R] → [Neg R] → [One R] → [Zero R] → Type u_2
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
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by37
Results whose statement or proof uses this declaration.
- FirstOrder.Ring.realize_termOfFreeCommRingstatement and proof · cited by 5
- FirstOrder.Ring.realize_zerostatement and proof · cited by 5
- FirstOrder.Field.ACF_isCompleteproof · cited by 3
- FirstOrder.Field.compatibleRingOfModelFieldstatement · cited by 3
- FirstOrder.Ring.compatibleRingOfRingstatement · cited by 3
- FirstOrder.realize_genericPolyMapSurjOnOfInjOnstatement and proof · cited by 2
- FirstOrder.Ring.CompatibleRing.funMap_addstatement and proof · cited by 2
- FirstOrder.Ring.CompatibleRing.funMap_mulstatement and proof · cited by 2
- FirstOrder.Ring.CompatibleRing.funMap_negstatement and proof · cited by 2
- FirstOrder.Ring.CompatibleRing.funMap_onestatement and proof · cited by 2
- FirstOrder.Ring.CompatibleRing.funMap_zerostatement and proof · cited by 2
- FirstOrder.Field.charP_of_model_fieldOfCharstatement and proof · cited by 2