Theorem AdicCompletion.AdicCauchySequence.mk_eq_mk

Modification history

2024-05-18 21:23
Mathlib/RingTheory/AdicCompletion/Basic.lean
feat(RingTheory/AdicCompletion): add algebra instance (#12553) …
Added AdicCompletion.AdicCauchySequence.mk_eq_mkView on Github →