equal
deleted
inserted
replaced
477 ((-1)^(card E) * a^(card A) * gsetprod id A * (-1)^(card E))](mod p)"; |
477 ((-1)^(card E) * a^(card A) * gsetprod id A * (-1)^(card E))](mod p)"; |
478 by (rule zcong_scalar) |
478 by (rule zcong_scalar) |
479 then have "[gsetprod id A * (-1)^(card E) = gsetprod id A * |
479 then have "[gsetprod id A * (-1)^(card E) = gsetprod id A * |
480 (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"; |
480 (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"; |
481 apply (rule zcong_trans) |
481 apply (rule zcong_trans) |
482 by (simp add: a zmult_commute zmult_left_commute) |
482 by (simp add: a mult_commute mult_left_commute) |
483 then have "[gsetprod id A * (-1)^(card E) = gsetprod id A * |
483 then have "[gsetprod id A * (-1)^(card E) = gsetprod id A * |
484 a^(card A)](mod p)"; |
484 a^(card A)](mod p)"; |
485 apply (rule zcong_trans) |
485 apply (rule zcong_trans) |
486 by (simp add: aux) |
486 by (simp add: aux) |
487 with this zcong_cancel2 [of p "gsetprod id A" "-1 ^ card E" "a ^ card A"] |
487 with this zcong_cancel2 [of p "gsetprod id A" "-1 ^ card E" "a ^ card A"] |