Mathlib v3 is deprecated. Go to Mathlib v4

Theorem dense_of_nonempty_smul_invariant

Modification history

2021-11-16 15:57

src/dynamics/minimal.lean

feat(dynamics): define `{mul,add}_action.is_minimal` (#10311)

Added dense_of_nonempty_smul_invariant View on Github →