Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-16 15:57 f7807881

View on Github →

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

Estimated changes

Created src/dynamics/minimal.lean

added theorem dense_of_nonempty_smul_invariant

added theorem dense_range_smul

added theorem eq_empty_or_univ_of_smul_invariant_closed

added theorem is_compact.exists_finite_cover_smul

added theorem is_minimal_iff_closed_smul_invariant

added theorem is_open.Union_preimage_smul

added theorem is_open.Union_smul

added theorem is_open.exists_smul_mem

added theorem mul_action.dense_orbit

Modified src/group_theory/group_action/basic.lean

added theorem mul_action.orbit_nonempty