Theorems · Theorem · commutative algebra

WittVector.succNthValUnits.congr_simp

∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] (n : ℕ) (a a_1 : kˣ),
  a = a_1 →
    ∀ (A A_1 : WittVector p k),
      A = A_1 →
        ∀ (bs bs_1 : Fin (n + 1) → k),
          bs = bs_1 → WittVector.succNthValUnits n a A bs = WittVector.succNthValUnits n a_1 A_1 bs_1

Defined in: Mathlib.RingTheory.WittVector.DiscreteValuationRing
Cited by: 0 results in Mathlib
Foundations: Depth 116 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Fact CommRing CharP

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

CommRingstatement and proof · cited by 17,173
Unitsstatement and proof · cited by 2,804
Factstatement and proof · cited by 2,726
Nat.Primestatement and proof · cited by 2,059
CharPstatement and proof · cited by 478
WittVectorstatement and proof · cited by 227
WittVector.succNthValUnitsstatement and proof · cited by 2

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.