Mathlib v3 is deprecated. Go to Mathlib v4

Theorem commute.smul_left_iff₀

Modification history

2022-03-28 20:38
src/group_theory/group_action/group.lean
feat(group_theory/group_action): add `commute.smul_{left,right}[_iff]` lemmas (#13003) …
Added commute.smul_left_iff₀View on Github →