charP_iff_model_fieldOfChar — Mathlib

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

Похожие утверждения