English
If a type K carries a field structure and a compatible ring, and p is a prime or zero, then the theory fieldOfChar p models on K.
Русский
Если K обладает структурой поля и совместимой колец, и p — простое число или ноль, то теория fieldOfChar p моделируется на K.
LaTeX
$$model_hasChar_of_charP : (Theory.fieldOfChar p).Model K$$
Lean4
instance model_hasChar_of_charP [Field K] [CompatibleRing K] [CharP K p] : (Theory.fieldOfChar p).Model K :=
by
refine Language.Theory.model_union_iff.2 ⟨inferInstance, ?_⟩
cases CharP.char_is_prime_or_zero K p with
| inl hp => simp [hp.ne_zero, hp, Sentence.Realize]
| inr hp =>
subst hp
simp only [ite_true, Theory.model_iff, Set.mem_image, Set.mem_setOf_eq, Sentence.Realize, forall_exists_index,
and_imp, forall_apply_eq_imp_iff₂, Formula.realize_not, realize_eqZero,
← CharZero.charZero_iff_forall_prime_ne_zero]
exact CharP.charP_to_charZero K
