src/HOL/Algebra/Ring_Divisibility.thy
changeset 69798 f610115ca3d0
parent 69597 ff784d5a5bfb
child 70160 8e9100dcde52