Theorem MulAction.movedBy_mem_fixedBy_of_commute

Modification history