English
In a local ring, equal-characteristic results apply with respect to ℚ-algebras and MixedCharZero.
Русский
В локальном кольце равная характеристика применяется к ℚ-алгебре и MixedCharZero.
LaTeX
$$$[IsLocalRing R] \\Rightarrow \\text{(EqualCharZero}\\_local)\\,\\text{and}\\,\\text{MixedCharZero}$$$
Lean4
/-- In a local ring `R`, split any predicate over `R` into the three cases:
- *prime power* characteristic.
- equal characteristic zero.
- mixed characteristic `(0, p)`.
-/
theorem split_by_characteristic_localRing [IsLocalRing R] (h_pos : ∀ p : ℕ, IsPrimePow 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_ppow : IsPrimePow (p : ℕ) := or_iff_not_imp_left.mp (charP_zero_or_prime_power R p) p_pos
exact h_pos p p_ppow p_char
