equal
deleted
inserted
replaced
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 |