Theorem SModEq.smul'

Modification history

2025-12-11 08:08
Mathlib/LinearAlgebra/SModEq/Pointwise.lean
feat(RingTheory/Perfectoid): Fontaine's theta map is surjective (#26384) …
Added SModEq.smul'View on Github →