FirstOrder.Field.FieldAxiom.toProp_of_model

theorem FirstOrder.Field.FieldAxiom.toProp_of_model : ∀ {K : Type u_2} [inst : Add K] [inst_1 : Mul K] [inst_2 : Neg K] [inst_3 : Zero K] [inst_4 : One K] [inst_5 : FirstOrder.Ring.CompatibleRing K] [inst_6 : K ⊨ FirstOrder.Language.Theory.field] (ax : FirstOrder.Field.FieldAxiom), FirstOrder.Field.FieldAxiom.toProp K ax

This theorem states that for any type `K` that has addition, multiplication, negation, a zero, and a one, and is compatible with the ring language in the sense of first order logic, if `K` satisfies the first order theory of fields, then any field axiom (represented by `ax`) is valid in `K`. In other words, the property corresponding to the field axiom holds in `K`.

More concisely: If `K` is a type with additions, multiplications, negation, zero, and one, compatible with the ring language, and satisfies the first-order theory of fields in Lean 4, then every field axiom holds in `K`.