Basic

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

Statistics

Metric	Count
Definitions instIsAlgebraicRing, CompatibleRing, toStructure, addFunc, addOfRingStructure, compatibleRingOfRing, compatibleRingOfRingStructure, instAddTermRing, instFintypeSymbolsRing, instMulTermRing, instNegTermRing, instOneTermRing, instZeroTermRing, languageEquivEquivRingEquiv, mulFunc, mulOfRingStructure, negFunc, negOfRingStructure, oneFunc, oneOfRingStructure, zeroFunc, zeroOfRingStructure, instDecidableEqRingFunc, decEq, ringFunc	25
Theorems funMap_add, funMap_mul, funMap_neg, funMap_one, funMap_zero, add_def, card_ring, mul_def, neg_def, one_def, realize_add, realize_mul, realize_neg, realize_one, realize_zero, zero_def	16
Total	41

FirstOrder

Definitions

Name	Category	Theorems
instDecidableEqRingFunc 📖	CompOp	—
ringFunc 📖	CompData	—

FirstOrder.Language

Definitions

Name	Category	Theorems
instIsAlgebraicRing 📖	CompOp	—

FirstOrder.Ring

Definitions

Name	Category	Theorems
CompatibleRing 📖	CompData	—
addFunc 📖	CompOp	2 math math: CompatibleRing.funMap_add, add_def
addOfRingStructure 📖	CompOp	—
compatibleRingOfRing 📖	CompOp	—
compatibleRingOfRingStructure 📖	CompOp	—
instAddTermRing 📖	CompOp	2 math math: realize_add, add_def
instFintypeSymbolsRing 📖	CompOp	—
instMulTermRing 📖	CompOp	2 math math: mul_def, realize_mul
instNegTermRing 📖	CompOp	2 math math: realize_neg, neg_def
instOneTermRing 📖	CompOp	2 math math: realize_one, one_def
instZeroTermRing 📖	CompOp	2 math math: realize_zero, zero_def
languageEquivEquivRingEquiv 📖	CompOp	—
mulFunc 📖	CompOp	2 math math: mul_def, CompatibleRing.funMap_mul
mulOfRingStructure 📖	CompOp	—
negFunc 📖	CompOp	2 math math: neg_def, CompatibleRing.funMap_neg
negOfRingStructure 📖	CompOp	—
oneFunc 📖	CompOp	2 math math: CompatibleRing.funMap_one, one_def
oneOfRingStructure 📖	CompOp	—
zeroFunc 📖	CompOp	2 math math: CompatibleRing.funMap_zero, zero_def
zeroOfRingStructure 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_def 📖	mathematical	—	FirstOrder.Language.Term FirstOrder.Language.ring instAddTermRing FirstOrder.Language.Functions.apply₂ addFunc	—	—
card_ring 📖	mathematical	—	FirstOrder.Language.card FirstOrder.Language.ring Cardinal instOfNatAtLeastTwo Cardinal.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Cardinal.mk_fintype
mul_def 📖	mathematical	—	FirstOrder.Language.Term FirstOrder.Language.ring instMulTermRing FirstOrder.Language.Functions.apply₂ mulFunc	—	—
neg_def 📖	mathematical	—	FirstOrder.Language.Term FirstOrder.Language.ring instNegTermRing FirstOrder.Language.Functions.apply₁ negFunc	—	—
one_def 📖	mathematical	—	FirstOrder.Language.Term FirstOrder.Language.ring instOneTermRing FirstOrder.Language.Constants.term oneFunc	—	—
realize_add 📖	mathematical	—	FirstOrder.Language.Term.realize FirstOrder.Language.ring CompatibleRing.toStructure FirstOrder.Language.Term instAddTermRing	—	FirstOrder.Language.Term.realize_functions_apply₂ CompatibleRing.funMap_add Matrix.cons_val_fin_one
realize_mul 📖	mathematical	—	FirstOrder.Language.Term.realize FirstOrder.Language.ring CompatibleRing.toStructure FirstOrder.Language.Term instMulTermRing	—	FirstOrder.Language.Term.realize_functions_apply₂ CompatibleRing.funMap_mul Matrix.cons_val_fin_one
realize_neg 📖	mathematical	—	FirstOrder.Language.Term.realize FirstOrder.Language.ring CompatibleRing.toStructure FirstOrder.Language.Term instNegTermRing	—	FirstOrder.Language.Term.realize_functions_apply₁ CompatibleRing.funMap_neg Matrix.cons_val_fin_one
realize_one 📖	mathematical	—	FirstOrder.Language.Term.realize FirstOrder.Language.ring CompatibleRing.toStructure FirstOrder.Language.Term instOneTermRing	—	FirstOrder.Language.Term.realize_constants CompatibleRing.funMap_one Fin.isEmpty'
realize_zero 📖	mathematical	—	FirstOrder.Language.Term.realize FirstOrder.Language.ring CompatibleRing.toStructure FirstOrder.Language.Term instZeroTermRing	—	FirstOrder.Language.Term.realize_constants CompatibleRing.funMap_zero Fin.isEmpty'
zero_def 📖	mathematical	—	FirstOrder.Language.Term FirstOrder.Language.ring instZeroTermRing FirstOrder.Language.Constants.term zeroFunc	—	—

FirstOrder.Ring.CompatibleRing

Definitions

Name	Category	Theorems
toStructure 📖	CompOp	21 math math: FirstOrder.Ring.realize_neg, FirstOrder.Field.realize_genericMonicPolyHasRoot, FirstOrder.Field.realize_eqZero, FirstOrder.Ring.realize_termOfFreeCommRing, FirstOrder.Field.instModelACFOfCharPOfIsAlgClosed, funMap_mul, FirstOrder.Ring.realize_add, FirstOrder.Field.FieldAxiom.realize_toSentence_iff_toProp, funMap_one, funMap_add, FirstOrder.Ring.realize_mul, FirstOrder.Ring.realize_zero, FirstOrder.Ring.realize_one, FirstOrder.Field.instModelField, FirstOrder.realize_genericPolyMapSurjOnOfInjOn, funMap_neg, FirstOrder.Field.model_hasChar_of_charP, funMap_zero, FirstOrder.Ring.mvPolynomial_zeroLocus_definable, FirstOrder.Field.model_fieldOfChar_of_charP, FirstOrder.Field.charP_iff_model_fieldOfChar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
funMap_add 📖	mathematical	—	FirstOrder.Language.Structure.funMap FirstOrder.Language.ring toStructure FirstOrder.Ring.addFunc	—	—
funMap_mul 📖	mathematical	—	FirstOrder.Language.Structure.funMap FirstOrder.Language.ring toStructure FirstOrder.Ring.mulFunc	—	—
funMap_neg 📖	mathematical	—	FirstOrder.Language.Structure.funMap FirstOrder.Language.ring toStructure FirstOrder.Ring.negFunc	—	—
funMap_one 📖	mathematical	—	FirstOrder.Language.Structure.funMap FirstOrder.Language.ring toStructure FirstOrder.Ring.oneFunc	—	—
funMap_zero 📖	mathematical	—	FirstOrder.Language.Structure.funMap FirstOrder.Language.ring toStructure FirstOrder.Ring.zeroFunc	—	—

FirstOrder.instDecidableEqRingFunc

Definitions

Name	Category	Theorems
decEq 📖	CompOp	—

---

← Back to Index