src/HOL/Algebra/abstract/RingHomo.thy
changeset 29885 379e43e513c2
parent 27541 9e585e99b494
child 35849 b5522b51cb1e