English
For an integral domain R, the predicate P splits into prime-power, equal-zero, or mixed-case predictions.
Русский
Для интегрального домена R предикат P разбивается на три случая.
LaTeX
$$$\\text{split\_by\_characteristic\_domain}(R,h\\_pos,h\\_equal,h\\_mixed)$$$
Lean4
/-- In an `IsDomain R`, split any `Prop` over `R` into the three cases:
- *prime* characteristic.
- equal characteristic zero.
- mixed characteristic `(0, p)`.
-/
theorem split_by_characteristic_domain [IsDomain R] (h_pos : ∀ p : ℕ, Nat.Prime p → CharP R p → P)
(h_equal : Algebra ℚ R → P) (h_mixed : ∀ p : ℕ, Nat.Prime p → MixedCharZero R p → P) : P :=
by
refine split_by_characteristic R ?_ h_equal h_mixed
intro p p_pos p_char
have p_prime : Nat.Prime p := or_iff_not_imp_right.mp (CharP.char_is_prime_or_zero R p) p_pos
exact h_pos p p_prime p_char
