English
Split any predicate on R according to whether the characteristic is prime-power, zero or mixed with p.
Русский
Разделить предикат на R по характеристике: простая степень, ноль или смешанная с p.
LaTeX
$$$\\text{split\_by\_characteristic}(R,h\\_pos,h\\_equal,h\\_mixed)$$$
Lean4
/-- Split any `Prop` over `R` into the three cases:
- positive characteristic.
- equal characteristic zero.
- mixed characteristic `(0, p)`.
-/
theorem split_by_characteristic (h_pos : ∀ p : ℕ, p ≠ 0 → CharP R p → P) (h_equal : Algebra ℚ R → P)
(h_mixed : ∀ p : ℕ, Nat.Prime p → MixedCharZero R p → P) : P := by
cases CharP.exists R with
| intro p p_charP =>
by_cases h : p = 0
· rw [h] at p_charP
haveI h0 : CharZero R := CharP.charP_to_charZero R
exact split_equalCharZero_mixedCharZero R h_equal h_mixed
· exact h_pos p h p_charP
