Theorems · Theorem · commutative algebra

split_by_characteristic

∀ (R : Type u_1) [inst : CommRing R] {P : Prop},
  (∀ (p : ℕ), p ≠ 0 → CharP R p → P) → (∀ (a : Algebra ℚ R), P) → (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → P

Split any Prop over R into the three cases: - positive characteristic. - equal characteristic zero. - mixed characteristic (0, p).

Defined in

Mathlib.Algebra.CharP.MixedCharZero

Cited by

2 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing