Theorem set_smul_closure_subset

Modification history

2025-09-22 13:30
Mathlib/Topology/Algebra/ConstMulAction.lean
feat(ConstMulAction): prove `set_smul_closure_subset` (#29859) …
Added set_smul_closure_subsetView on Github →