Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-13 16:06 3578403f

View on Github →

feat(*/{group,mul}_action): more lemmas (#10308)

  • add several lemmas about orbits and pointwise scalar multiplication;
  • generalize mul_action.orbit.mul_action to a monoid action;
  • more lemmas about pretransitive actions, use to_additive more;
  • add dot notation lemmas is_open.smul and is_closed.smul.

Estimated changes

deleted theorem add_action.exists_vadd_eq
modified theorem mul_action.mem_orbit_smul
added theorem mul_action.orbit_smul
added theorem mul_action.smul_orbit
added theorem is_closed.smul
added theorem is_open.smul
added theorem smul_closure_subset