Commit 2024-04-04 22:42 21e0675e

View on Github →

feat(GroupTheory/GroupAction/Basic): various orbit lemmas (#11286) Add various miscellaneous lemmas about orbits, mainly about orbits under the subgroup / submonoid action. From AperiodicMonotilesLean.

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

added theorem MulAction.mem_orbit_of_mem_orbit_subgroup

added theorem MulAction.mem_orbit_of_mem_orbit_submonoid

added theorem MulAction.mem_orbit_symm

added theorem MulAction.mem_subgroup_orbit_iff

added theorem MulAction.orbitRel_subgroup_le

added theorem MulAction.orbit_subgroup_subset

added theorem MulAction.orbit_submonoid_subset