Commit 2023-06-27 01:24 07ec5c2b

View on Github →

chore: forward port #18862 (#5497)

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

added theorem MulAction.orbitRel_apply

Modified Mathlib/GroupTheory/GroupAction/ConjAct.lean

added theorem ConjAct.mem_orbit_conjAct

added theorem ConjAct.orbitRel_conjAct

Modified Mathlib/GroupTheory/Subgroup/Basic.lean

added theorem IsConj.eq_of_left_mem_center

added theorem IsConj.eq_of_right_mem_center