Theorem AdicCompletion.val_sum

Modification history

2024-12-08 07:41
Mathlib/RingTheory/AdicCompletion/Basic.lean
chore(AdicCompletion): generalise algebra instance to separate rings (#19466) …
Modified AdicCompletion.val_sumView on Github →
2024-07-11 16:02
Mathlib/RingTheory/AdicCompletion/Basic.lean
chore(RingTheory/AdicCompletion): manual instances (#14534) …
Modified AdicCompletion.val_sumView on Github →
2024-06-11 14:59
Mathlib/RingTheory/AdicCompletion/Functoriality.lean
feat(RingTheory/AdicCompletion): functoriality (#12543) …
Added AdicCompletion.val_sumView on Github →