Theorems · Theorem · commutative algebra

WittVector.le_coeff_eq_iff_le_sub_coeff_eq_zero

∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] {x y : WittVector p k} {n : ℕ},
  (∀ i < n, x.coeff i = y.coeff i) ↔ ∀ i < n, (x - y).coeff i = 0

Defined in

Mathlib.RingTheory.WittVector.Complete

Cited by

1 results in Mathlib

Foundations

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

Assumes

FactCommRing