src/HOL/Algebra/Divisibility.thy
changeset 28600 54352ed7114f
parent 28599 12d914277b8d
child 28823 dcbef866c9e2
equal deleted inserted replaced
28599:12d914277b8d 28600:54352ed7114f
  1342 using wf
  1342 using wf
  1343 unfolding wfactors_def
  1343 unfolding wfactors_def
  1344 by (fast dest: e)
  1344 by (fast dest: e)
  1345 
  1345 
  1346 lemma (in monoid) factorsI:
  1346 lemma (in monoid) factorsI:
  1347   fixes G (structure)
       
  1348   assumes "\<forall>f\<in>set fs. irreducible G f"
  1347   assumes "\<forall>f\<in>set fs. irreducible G f"
  1349     and "foldr (op \<otimes>) fs \<one> = a"
  1348     and "foldr (op \<otimes>) fs \<one> = a"
  1350   shows "factors G fs a"
  1349   shows "factors G fs a"
  1351 using assms
  1350 using assms
  1352 unfolding factors_def
  1351 unfolding factors_def