Theorem AdicCompletion.restrictScalars_range_ofPowSMul_eq_ker_eval

Modification history

2026-03-25 23:27
Mathlib/RingTheory/AdicCompletion/Completeness.lean
feat(RingTheory/AdicCompletion): completeness of `AdicCompletion` (#35670) …
Added AdicCompletion.restrictScalars_range_ofPowSMul_eq_ker_evalView on Github →