Commit 2024-05-01 18:59 94b9da4b

View on Github →

feat(RingTheory/AdicCompletion): refactor and expand API (#12516) Refactors and expands the API for adic completions. More precisely:

  • Renames adicCompletion to AdicCompletion.
  • Redefines adicCompletion in terms of a transitionMap.
  • Introduces AdicCauchySequence as the module of I-adic Cauchy sequences.
  • Provides a surjective linear map AdicCauchySequence I M →ₗ[R] AdicCompletion I M and an induction principle for AdicCompletion I M for that.

Estimated changes

added theorem AdicCompletion.eval_of
added theorem AdicCompletion.ext
added theorem AdicCompletion.ext_iff
added theorem AdicCompletion.val_add
added theorem AdicCompletion.val_sub
added def AdicCompletion
deleted theorem adicCompletion.coe_eval
deleted def adicCompletion.eval
deleted theorem adicCompletion.eval_apply
deleted theorem adicCompletion.eval_of
deleted theorem adicCompletion.ext
deleted def adicCompletion.of
deleted theorem adicCompletion.of_apply
deleted theorem adicCompletion.range_eval
deleted def adicCompletion