Theorem AdicCompletion.val_neg_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_neg_applyView on Github →