Theorem smul_mem_closure_star_mul

Modification history

2025-08-26 23:57

Mathlib/Algebra/Order/Star/Basic.lean

refactor: generalise monotonicity of scalar multiplication to star-semimodules (#28852)

Added smul_mem_closure_star_mul View on Github →