Theorems · Definition · logic and foundations

FirstOrder.Field.FieldAxiom.casesOn

{motive : FirstOrder.Field.FieldAxiom → Sort u} →
  (t : FirstOrder.Field.FieldAxiom) →
    motive FirstOrder.Field.FieldAxiom.addAssoc →
      motive FirstOrder.Field.FieldAxiom.zeroAdd →
        motive FirstOrder.Field.FieldAxiom.negAddCancel →
          motive FirstOrder.Field.FieldAxiom.mulAssoc →
            motive FirstOrder.Field.FieldAxiom.mulComm →
              motive FirstOrder.Field.FieldAxiom.oneMul →
                motive FirstOrder.Field.FieldAxiom.existsInv →
                  motive FirstOrder.Field.FieldAxiom.leftDistrib →
                    motive FirstOrder.Field.FieldAxiom.existsPairNE → motive t

Defined in: Mathlib.ModelTheory.Algebra.Field.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 3 from the axioms · uses no axioms

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

FirstOrder.Field.FieldAxiomstatement and proof · cited by 11

Cited by3

Results whose statement or proof uses this declaration.

FirstOrder.Field.FieldAxiom.realize_toSentence_iff_toPropproof · cited by 1
FirstOrder.Field.FieldAxiom.ctorIdxproof · cited by 0
FirstOrder.Field.FieldAxiom.ctorElimproof · cited by 0