Theorems · Theorem · commutative algebra
TruncatedWittVector.ext
∀ {p n : ℕ} {R : Type u_1} {x y : TruncatedWittVector p n R},
(∀ (i : Fin n), TruncatedWittVector.coeff i x = TruncatedWittVector.coeff i y) → x = y- Defined in
- Mathlib.RingTheory.WittVector.Truncated
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TruncatedWittVectorstatement and proof · cited by 56
- TruncatedWittVector.coeffstatement and proof · cited by 14
Cited by7
Results whose statement or proof uses this declaration.
- TruncatedWittVector.out_injectiveproof · cited by 7
- WittVector.truncate_mk'proof · cited by 1
- TruncatedWittVector.ext_iffproof · cited by 1
- TruncatedWittVector.mk_coeffproof · cited by 1
- WittVector.frobenius_frobeniusRotationproof · cited by 1
- WittVector.le_coeff_eq_iff_le_sub_coeff_eq_zeroproof · cited by 1
- WittVector.truncate_liftFunproof · cited by 1