Commit 2025-09-22 13:30 5c1fe161
View on Github →feat(ConstMulAction): prove set_smul_closure_subset (#29859)
Cherry-picked from #24163.
It is useful for the proof of tangentConeAt_closure
for the pending new definition of tangentConeAt.
feat(ConstMulAction): prove set_smul_closure_subset (#29859)
Cherry-picked from #24163.
It is useful for the proof of tangentConeAt_closure
for the pending new definition of tangentConeAt.