Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/NumberTheory/Gauss.thy
changeset 16733 236dfafbeb63
parent 16663 13e9c402308b
child 16775 c1b87ef4a1c3
equal deleted inserted replaced
16732:1bbe526a552c 16733:236dfafbeb63 
   457     then have "[setprod id A = ((-1)^(card E) *
 
   457     then have "[setprod id A = ((-1)^(card E) *
 
   458         (setprod id ((%x. x * a) ` A)))] (mod p)"
 
   458         (setprod id ((%x. x * a) ` A)))] (mod p)"
 
   459       by (simp add: B_def)
 
   459       by (simp add: B_def)
 
   460     then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))] 
   460     then have "[setprod id A = ((-1)^(card E) * (setprod (%x. x * a) A))] 
   461         (mod p)"
 
   461         (mod p)"
 
   462       apply (rule zcong_trans)
 
   462       by(simp add:finite_A inj_on_xa_A setprod_reindex_id[symmetric])
 
   463       by (simp add: finite_A inj_on_xa_A setprod_reindex_id zcong_scalar2)
 
       
   464     moreover have "setprod (%x. x * a) A = 
   463     moreover have "setprod (%x. x * a) A = 
   465         setprod (%x. a) A * setprod id A"
 
   464         setprod (%x. a) A * setprod id A"
 
   466       by (insert finite_A, induct set: Finites, auto)
 
   465       by (insert finite_A, induct set: Finites, auto)
 
   467     ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A * 
   466     ultimately have "[setprod id A = ((-1)^(card E) * (setprod (%x. a) A * 
   468         setprod id A))] (mod p)"
 
   467         setprod id A))] (mod p)"
isabelle