src/HOL/Algebra/FiniteProduct.thy
 changeset 32960 69916a850301 parent 32693 6c6b1ba5e71e child 35054 a5db9779b026
```     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 17 01:05:59 2009 +0200
1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 17 14:43:18 2009 +0200
1.3 @@ -423,17 +423,17 @@
1.4        then have "finprod G f A = finprod G f (insert x B)" by simp
1.5        also from insert have "... = f x \<otimes> finprod G f B"
1.6        proof (intro finprod_insert)
1.7 -	show "finite B" by fact
1.8 +        show "finite B" by fact
1.9        next
1.10 -	show "x ~: B" by fact
1.11 +        show "x ~: B" by fact
1.12        next
1.13 -	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
1.14 -	  "g \<in> insert x B \<rightarrow> carrier G"
1.15 -	thus "f \<in> B -> carrier G" by fastsimp
1.16 +        assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
1.17 +          "g \<in> insert x B \<rightarrow> carrier G"
1.18 +        thus "f \<in> B -> carrier G" by fastsimp
1.19        next
1.20 -	assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
1.21 -	  "g \<in> insert x B \<rightarrow> carrier G"
1.22 -	thus "f x \<in> carrier G" by fastsimp
1.23 +        assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
1.24 +          "g \<in> insert x B \<rightarrow> carrier G"
1.25 +        thus "f x \<in> carrier G" by fastsimp
1.26        qed
1.27        also from insert have "... = g x \<otimes> finprod G g B" by fastsimp
1.28        also from insert have "... = finprod G g (insert x B)"
```
{"ft_lang_label":"__label__en","ft_lang_prob":0.6268301,"math_prob":0.96698284,"size":1332,"snap":"2020-34-2020-40","text_gpt3_token_len":519,"char_repetition_ratio":0.17018072,"word_repetition_ratio":0.37226278,"special_character_ratio":0.475976,"punctuation_ratio":0.18208092,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.97576857,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2020-08-10T07:04:35Z\",\"WARC-Record-ID\":\"<urn:uuid:feafc685-82ce-4120-a466-9e323a8b4aa5>\",\"Content-Length\":\"6965\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:747eebfd-3a6a-4ad5-b521-bf5d9a7a0ee5>\",\"WARC-Concurrent-To\":\"<urn:uuid:f243fa30-f157-4964-8553-1f79891e4243>\",\"WARC-IP-Address\":\"131.159.46.82\",\"WARC-Target-URI\":\"http://isabelle.in.tum.de/repos/isabelle/diff/69916a850301/src/HOL/Algebra/FiniteProduct.thy\",\"WARC-Payload-Digest\":\"sha1:XM35AW23PL6Y6WCSOLOBSQFIDERJ7DIQ\",\"WARC-Block-Digest\":\"sha1:IGPPTKVYHRDIB4ITCOSLTGNSFZ5NWYKE\",\"WARC-Identified-Payload-Type\":\"application/xhtml+xml\",\"warc_filename\":\"/cc_download/warc_2020/CC-MAIN-2020-34/CC-MAIN-2020-34_segments_1596439738609.73_warc_CC-MAIN-20200810042140-20200810072140-00284.warc.gz\"}"}