English
For a field K, CharP K p holds iff the theory fieldOfChar p models on K.
Русский
Для поля K характеристика p верна тогда и только тогда, когда теория fieldOfChar p моделируется на K.
LaTeX
$$CharP K p ↔ (Theory.fieldOfChar p).Model K$$
Lean4
theorem charP_iff_model_fieldOfChar [Field K] [CompatibleRing K] : (Theory.fieldOfChar p).Model K ↔ CharP K p :=
by
simp only [Theory.fieldOfChar, Theory.model_union_iff, (show (Theory.field.Model K) by infer_instance), true_and]
split_ifs with hp0 hp
· subst hp0
simp only [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 ⟨fun _ => CharP.ofCharZero _, fun _ => CharP.charP_to_charZero K⟩
·
simp only [Theory.model_iff, Set.mem_singleton_iff, Sentence.Realize, forall_eq, realize_eqZero,
← CharP.charP_iff_prime_eq_zero hp]
· simp only [Theory.model_iff, Set.mem_singleton_iff, Sentence.Realize, forall_eq, Formula.realize_bot, false_iff]
intro H
cases (CharP.char_is_prime_or_zero K p) <;> simp_all