Theorem SModEq.restrictScalars

Modification history

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