split_equalCharZero_mixedCharZero

English

Split any predicate on R by characteristic into prime-power, equal-zero, or mixed with p.

Русский

Разделить произвольное предикатное высказывание над R на три случая: простая величина, равная нулю характеристика и смешанная (0,p).

LaTeX

$$$\\text{split_by_characteristic}(R,P,h\\_equal,h\\_mixed)$$$

Lean4

/-- Split a `Prop` in characteristic zero into equal and mixed characteristic. -/
theorem split_equalCharZero_mixedCharZero [CharZero R] (h_equal : Algebra ℚ R → P)
    (h_mixed : ∀ p : ℕ, Nat.Prime p → MixedCharZero R p → P) : P :=
  by
  by_cases h : ∃ p > 0, MixedCharZero R p
  · rcases h with ⟨p, ⟨H, hp⟩⟩
    rw [← MixedCharZero.reduce_to_p_prime] at h_mixed
    exact h_mixed p H hp
  · apply h_equal
    rw [← isEmpty_algebraRat_iff_mixedCharZero, not_isEmpty_iff] at h
    exact h.some

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