Mathlib v3 is deprecated. Go to Mathlib v4

Theorem eq_empty_or_univ_of_smul_invariant_closed

Modification history

2021-11-16 15:57
src/dynamics/minimal.lean
feat(dynamics): define `{mul,add}_action.is_minimal` (#10311)
Added eq_empty_or_univ_of_smul_invariant_closedView on Github →