Theorem DivisibleHull.mk_eq_mk_iff_smul_eq_smul

Modification history

2025-10-09 12:15
Mathlib/GroupTheory/DivisibleHull.lean
feat(GroupTheory): add DivisibleHull (#29275) …
Added DivisibleHull.mk_eq_mk_iff_smul_eq_smulView on Github →