Theorem AdicCompletion.val_sum_apply

Modification history

2024-12-08 07:41
Mathlib/RingTheory/AdicCompletion/Basic.lean
chore(AdicCompletion): generalise algebra instance to separate rings (#19466) …
Added AdicCompletion.val_sum_applyView on Github →