src/HOL/Algebra/Multiplicative_Group.thy
changeset 82124 1eda03781f76
parent 81438 95c9af7483b1
equal deleted inserted replaced
82123:c30b6eff8fa1 82124:1eda03781f76