Theorem IsClosed.smul₀

Modification history

2024-03-10 18:54

Mathlib/Topology/Algebra/ConstMulAction.lean

feat(ConstMulAction): add `closure_smul₀'`, generalize (#10860) …

Modified IsClosed.smul₀ View on Github →

2023-08-10 19:52

Mathlib/Topology/Algebra/ConstMulAction.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified IsClosed.smul₀ View on Github →

2023-02-02 17:16

Mathlib/Topology/Algebra/ConstMulAction.lean

feat: port Topology.Algebra.ConstMulAction (#2012)

Added IsClosed.smul₀ View on Github →