Theorem SModEq.of_toAddSubgroup_le

Modification history

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