Commit 2023-07-01 12:39 3282e2f7

View on Github →

chore: tidy various files (#5628)

Estimated changes

Modified Mathlib/Algebra/Category/FGModuleCat/Basic.lean

Modified Mathlib/Algebra/CharP/Basic.lean

Modified Mathlib/AlgebraicGeometry/AffineScheme.lean

Modified Mathlib/AlgebraicGeometry/Gluing.lean

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/AlgebraicGeometry/Pullbacks.lean

Modified Mathlib/Analysis/Normed/Group/Basic.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Even.lean

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean

Modified Mathlib/NumberTheory/ModularForms/SlashInvariantForms.lean

Modified Mathlib/NumberTheory/ZetaFunction.lean

Modified Mathlib/RingTheory/WittVector/Compare.lean

deleted theorem TruncatedWittVector.card_zMod

added theorem TruncatedWittVector.card_zmod

deleted theorem TruncatedWittVector.charP_zMod

added theorem TruncatedWittVector.charP_zmod

added def WittVector.toZModPow

added theorem WittVector.toZModPow_compat

deleted def WittVector.toZmodPow

deleted theorem WittVector.toZmodPow_compat

Modified Mathlib/RingTheory/WittVector/Identities.lean

modified theorem WittVector.coeff_p_pow

modified theorem WittVector.coeff_p_pow_eq_zero

Modified Mathlib/RingTheory/WittVector/Truncated.lean