chore(ring_theory/witt_vector): fix a docstring (#9575)

leanprover-community · Oct 6, 2021 · 6abd6f2 · 6abd6f2
1 parent 850d5d2
commit 6abd6f2
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/src/ring_theory/witt_vector/frobenius.lean b/src/ring_theory/witt_vector/frobenius.lean
@@ -79,7 +79,7 @@ private def pnat_multiplicity (n : ℕ+) : ℕ :=
 local notation `v` := pnat_multiplicity
 
 /-- An auxiliary polynomial over the integers, that satisfies
-`(frobenius_poly_aux p n - X n ^ p) / p = frobenius_poly p n`.
+`p * (frobenius_poly_aux p n) + X n ^ p = frobenius_poly p n`.
 This makes it easy to show that `frobenius_poly p n` is congruent to `X n ^ p`
 modulo `p`. -/
 noncomputable def frobenius_poly_aux : ℕ → mv_polynomial ℕ ℤ

diff --git a/src/ring_theory/witt_vector/structure_polynomial.lean b/src/ring_theory/witt_vector/structure_polynomial.lean
@@ -180,11 +180,11 @@ begin
   exact pow_ne_zero _ (nat.cast_ne_zero.2 hp.1.ne_zero),
 end
 
-/-- `witt_structure_int Φ` is a family of polynomials `ℕ → mv_polynomial (idx × ℕ) ℚ`
+/-- `witt_structure_int Φ` is a family of polynomials `ℕ → mv_polynomial (idx × ℕ) ℤ`
 that are uniquely characterised by the property that
 ```
-bind₁ (witt_structure_int p Φ) (witt_polynomial p ℚ n) =
-bind₁ (λ i, (rename (prod.mk i) (witt_polynomial p ℚ n))) Φ
+bind₁ (witt_structure_int p Φ) (witt_polynomial p ℤ n) =
+bind₁ (λ i, (rename (prod.mk i) (witt_polynomial p ℤ n))) Φ
 ```
 In other words: evaluating the `n`-th Witt polynomial on the family `witt_structure_int Φ`
 is the same as evaluating `Φ` on the (appropriately renamed) `n`-th Witt polynomials.