Commit 2023-09-15 17:12 42f80cb4

View on Github →

feat(ModelTheory): the language of rings (#7185)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Algebra/Ring/Basic.lean

added def FirstOrder.Language.ring

added def FirstOrder.Ring.addOfRingStructure

added theorem FirstOrder.Ring.add_def

added theorem FirstOrder.Ring.card_ring

added def FirstOrder.Ring.compatibleRingOfRing

added def FirstOrder.Ring.compatibleRingOfRingStructure

added def FirstOrder.Ring.languageEquivEquivRingEquiv

added def FirstOrder.Ring.mulOfRingStructure

added theorem FirstOrder.Ring.mul_def

added def FirstOrder.Ring.negOfRingStructure

added theorem FirstOrder.Ring.neg_def

added def FirstOrder.Ring.oneOfRingStructure

added theorem FirstOrder.Ring.one_def

added theorem FirstOrder.Ring.realize_add

added theorem FirstOrder.Ring.realize_mul

added theorem FirstOrder.Ring.realize_neg

added theorem FirstOrder.Ring.realize_one

added theorem FirstOrder.Ring.realize_zero

added def FirstOrder.Ring.zeroOfRingStructure

added theorem FirstOrder.Ring.zero_def

added inductive FirstOrder.ringFunc