src/HOL/Algebra/QuotRing.thy
 author hoelzl Tue Mar 26 12:20:58 2013 +0100 (2013-03-26) changeset 51526 155263089e7b parent 45005 0d2d59525912 child 61382 efac889fccbc permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
 wenzelm@35849 ` 1` ```(* Title: HOL/Algebra/QuotRing.thy ``` wenzelm@35849 ` 2` ``` Author: Stephan Hohe ``` ballarin@20318 ` 3` ```*) ``` ballarin@20318 ` 4` ballarin@20318 ` 5` ```theory QuotRing ``` ballarin@20318 ` 6` ```imports RingHom ``` ballarin@20318 ` 7` ```begin ``` ballarin@20318 ` 8` ballarin@27717 ` 9` ```section {* Quotient Rings *} ``` ballarin@27717 ` 10` ballarin@20318 ` 11` ```subsection {* Multiplication on Cosets *} ``` ballarin@20318 ` 12` wenzelm@45005 ` 13` ```definition rcoset_mult :: "[('a, _) ring_scheme, 'a set, 'a set, 'a set] \ 'a set" ``` wenzelm@23463 ` 14` ``` ("[mod _:] _ \\ _" [81,81,81] 80) ``` wenzelm@35848 ` 15` ``` where "rcoset_mult R I A B = (\a\A. \b\B. I +>\<^bsub>R\<^esub> (a \\<^bsub>R\<^esub> b))" ``` ballarin@20318 ` 16` ballarin@20318 ` 17` ballarin@20318 ` 18` ```text {* @{const "rcoset_mult"} fulfils the properties required by ``` ballarin@20318 ` 19` ``` congruences *} ``` ballarin@20318 ` 20` ```lemma (in ideal) rcoset_mult_add: ``` wenzelm@45005 ` 21` ``` "x \ carrier R \ y \ carrier R \ [mod I:] (I +> x) \ (I +> y) = I +> (x \ y)" ``` wenzelm@45005 ` 22` ``` apply rule ``` wenzelm@45005 ` 23` ``` apply (rule, simp add: rcoset_mult_def, clarsimp) ``` wenzelm@45005 ` 24` ``` defer 1 ``` wenzelm@45005 ` 25` ``` apply (rule, simp add: rcoset_mult_def) ``` wenzelm@45005 ` 26` ``` defer 1 ``` ballarin@20318 ` 27` ```proof - ``` ballarin@20318 ` 28` ``` fix z x' y' ``` ballarin@20318 ` 29` ``` assume carr: "x \ carrier R" "y \ carrier R" ``` wenzelm@45005 ` 30` ``` and x'rcos: "x' \ I +> x" ``` wenzelm@45005 ` 31` ``` and y'rcos: "y' \ I +> y" ``` wenzelm@45005 ` 32` ``` and zrcos: "z \ I +> x' \ y'" ``` wenzelm@45005 ` 33` wenzelm@45005 ` 34` ``` from x'rcos have "\h\I. x' = h \ x" ``` wenzelm@45005 ` 35` ``` by (simp add: a_r_coset_def r_coset_def) ``` wenzelm@45005 ` 36` ``` then obtain hx where hxI: "hx \ I" and x': "x' = hx \ x" ``` wenzelm@45005 ` 37` ``` by fast+ ``` ballarin@20318 ` 38` wenzelm@45005 ` 39` ``` from y'rcos have "\h\I. y' = h \ y" ``` wenzelm@45005 ` 40` ``` by (simp add: a_r_coset_def r_coset_def) ``` wenzelm@45005 ` 41` ``` then obtain hy where hyI: "hy \ I" and y': "y' = hy \ y" ``` wenzelm@45005 ` 42` ``` by fast+ ``` ballarin@20318 ` 43` wenzelm@45005 ` 44` ``` from zrcos have "\h\I. z = h \ (x' \ y')" ``` wenzelm@45005 ` 45` ``` by (simp add: a_r_coset_def r_coset_def) ``` wenzelm@45005 ` 46` ``` then obtain hz where hzI: "hz \ I" and z: "z = hz \ (x' \ y')" ``` wenzelm@45005 ` 47` ``` by fast+ ``` ballarin@20318 ` 48` ballarin@20318 ` 49` ``` note carr = carr hxI[THEN a_Hcarr] hyI[THEN a_Hcarr] hzI[THEN a_Hcarr] ``` ballarin@20318 ` 50` ballarin@20318 ` 51` ``` from z have "z = hz \ (x' \ y')" . ``` wenzelm@45005 ` 52` ``` also from x' y' have "\ = hz \ ((hx \ x) \ (hy \ y))" by simp ``` wenzelm@45005 ` 53` ``` also from carr have "\ = (hz \ (hx \ (hy \ y)) \ x \ hy) \ x \ y" by algebra ``` wenzelm@45005 ` 54` ``` finally have z2: "z = (hz \ (hx \ (hy \ y)) \ x \ hy) \ x \ y" . ``` ballarin@20318 ` 55` wenzelm@45005 ` 56` ``` from hxI hyI hzI carr have "hz \ (hx \ (hy \ y)) \ x \ hy \ I" ``` wenzelm@45005 ` 57` ``` by (simp add: I_l_closed I_r_closed) ``` ballarin@20318 ` 58` wenzelm@45005 ` 59` ``` with z2 have "\h\I. z = h \ x \ y" by fast ``` wenzelm@45005 ` 60` ``` then show "z \ I +> x \ y" by (simp add: a_r_coset_def r_coset_def) ``` ballarin@20318 ` 61` ```next ``` ballarin@20318 ` 62` ``` fix z ``` ballarin@20318 ` 63` ``` assume xcarr: "x \ carrier R" ``` wenzelm@45005 ` 64` ``` and ycarr: "y \ carrier R" ``` wenzelm@45005 ` 65` ``` and zrcos: "z \ I +> x \ y" ``` wenzelm@45005 ` 66` ``` from xcarr have xself: "x \ I +> x" by (intro a_rcos_self) ``` wenzelm@45005 ` 67` ``` from ycarr have yself: "y \ I +> y" by (intro a_rcos_self) ``` wenzelm@45005 ` 68` ``` show "\a\I +> x. \b\I +> y. z \ I +> a \ b" ``` wenzelm@45005 ` 69` ``` using xself and yself and zrcos by fast ``` ballarin@20318 ` 70` ```qed ``` ballarin@20318 ` 71` ballarin@20318 ` 72` ballarin@20318 ` 73` ```subsection {* Quotient Ring Definition *} ``` ballarin@20318 ` 74` wenzelm@45005 ` 75` ```definition FactRing :: "[('a,'b) ring_scheme, 'a set] \ ('a set) ring" ``` wenzelm@45005 ` 76` ``` (infixl "Quot" 65) ``` wenzelm@35848 ` 77` ``` where "FactRing R I = ``` wenzelm@45005 ` 78` ``` \carrier = a_rcosets\<^bsub>R\<^esub> I, mult = rcoset_mult R I, ``` wenzelm@45005 ` 79` ``` one = (I +>\<^bsub>R\<^esub> \\<^bsub>R\<^esub>), zero = I, add = set_add R\" ``` ballarin@20318 ` 80` ballarin@20318 ` 81` ballarin@20318 ` 82` ```subsection {* Factorization over General Ideals *} ``` ballarin@20318 ` 83` ballarin@20318 ` 84` ```text {* The quotient is a ring *} ``` wenzelm@45005 ` 85` ```lemma (in ideal) quotient_is_ring: "ring (R Quot I)" ``` ballarin@20318 ` 86` ```apply (rule ringI) ``` ballarin@20318 ` 87` ``` --{* abelian group *} ``` ballarin@20318 ` 88` ``` apply (rule comm_group_abelian_groupI) ``` ballarin@20318 ` 89` ``` apply (simp add: FactRing_def) ``` ballarin@20318 ` 90` ``` apply (rule a_factorgroup_is_comm_group[unfolded A_FactGroup_def']) ``` ballarin@20318 ` 91` ``` --{* mult monoid *} ``` ballarin@20318 ` 92` ``` apply (rule monoidI) ``` ballarin@20318 ` 93` ``` apply (simp_all add: FactRing_def A_RCOSETS_def RCOSETS_def ``` ballarin@20318 ` 94` ``` a_r_coset_def[symmetric]) ``` ballarin@20318 ` 95` ``` --{* mult closed *} ``` ballarin@20318 ` 96` ``` apply (clarify) ``` ballarin@20318 ` 97` ``` apply (simp add: rcoset_mult_add, fast) ``` wenzelm@21502 ` 98` ``` --{* mult @{text one_closed} *} ``` wenzelm@45005 ` 99` ``` apply force ``` ballarin@20318 ` 100` ``` --{* mult assoc *} ``` ballarin@20318 ` 101` ``` apply clarify ``` ballarin@20318 ` 102` ``` apply (simp add: rcoset_mult_add m_assoc) ``` ballarin@20318 ` 103` ``` --{* mult one *} ``` ballarin@20318 ` 104` ``` apply clarify ``` wenzelm@45005 ` 105` ``` apply (simp add: rcoset_mult_add) ``` ballarin@20318 ` 106` ``` apply clarify ``` wenzelm@45005 ` 107` ``` apply (simp add: rcoset_mult_add) ``` ballarin@20318 ` 108` ``` --{* distr *} ``` ballarin@20318 ` 109` ``` apply clarify ``` ballarin@20318 ` 110` ``` apply (simp add: rcoset_mult_add a_rcos_sum l_distr) ``` ballarin@20318 ` 111` ```apply clarify ``` ballarin@20318 ` 112` ```apply (simp add: rcoset_mult_add a_rcos_sum r_distr) ``` ballarin@20318 ` 113` ```done ``` ballarin@20318 ` 114` ballarin@20318 ` 115` ballarin@20318 ` 116` ```text {* This is a ring homomorphism *} ``` ballarin@20318 ` 117` wenzelm@45005 ` 118` ```lemma (in ideal) rcos_ring_hom: "(op +> I) \ ring_hom R (R Quot I)" ``` ballarin@20318 ` 119` ```apply (rule ring_hom_memI) ``` ballarin@20318 ` 120` ``` apply (simp add: FactRing_def a_rcosetsI[OF a_subset]) ``` ballarin@20318 ` 121` ``` apply (simp add: FactRing_def rcoset_mult_add) ``` ballarin@20318 ` 122` ``` apply (simp add: FactRing_def a_rcos_sum) ``` ballarin@20318 ` 123` ```apply (simp add: FactRing_def) ``` ballarin@20318 ` 124` ```done ``` ballarin@20318 ` 125` wenzelm@45005 ` 126` ```lemma (in ideal) rcos_ring_hom_ring: "ring_hom_ring R (R Quot I) (op +> I)" ``` ballarin@20318 ` 127` ```apply (rule ring_hom_ringI) ``` ballarin@20318 ` 128` ``` apply (rule is_ring, rule quotient_is_ring) ``` ballarin@20318 ` 129` ``` apply (simp add: FactRing_def a_rcosetsI[OF a_subset]) ``` ballarin@20318 ` 130` ``` apply (simp add: FactRing_def rcoset_mult_add) ``` ballarin@20318 ` 131` ``` apply (simp add: FactRing_def a_rcos_sum) ``` ballarin@20318 ` 132` ```apply (simp add: FactRing_def) ``` ballarin@20318 ` 133` ```done ``` ballarin@20318 ` 134` ballarin@20318 ` 135` ```text {* The quotient of a cring is also commutative *} ``` ballarin@20318 ` 136` ```lemma (in ideal) quotient_is_cring: ``` ballarin@27611 ` 137` ``` assumes "cring R" ``` ballarin@20318 ` 138` ``` shows "cring (R Quot I)" ``` ballarin@27611 ` 139` ```proof - ``` ballarin@29237 ` 140` ``` interpret cring R by fact ``` wenzelm@45005 ` 141` ``` show ?thesis ``` wenzelm@45005 ` 142` ``` apply (intro cring.intro comm_monoid.intro comm_monoid_axioms.intro) ``` wenzelm@45005 ` 143` ``` apply (rule quotient_is_ring) ``` wenzelm@45005 ` 144` ``` apply (rule ring.axioms[OF quotient_is_ring]) ``` wenzelm@45005 ` 145` ``` apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric]) ``` wenzelm@45005 ` 146` ``` apply clarify ``` wenzelm@45005 ` 147` ``` apply (simp add: rcoset_mult_add m_comm) ``` wenzelm@45005 ` 148` ``` done ``` ballarin@27611 ` 149` ```qed ``` ballarin@20318 ` 150` ballarin@20318 ` 151` ```text {* Cosets as a ring homomorphism on crings *} ``` ballarin@20318 ` 152` ```lemma (in ideal) rcos_ring_hom_cring: ``` ballarin@27611 ` 153` ``` assumes "cring R" ``` ballarin@20318 ` 154` ``` shows "ring_hom_cring R (R Quot I) (op +> I)" ``` ballarin@27611 ` 155` ```proof - ``` ballarin@29237 ` 156` ``` interpret cring R by fact ``` wenzelm@45005 ` 157` ``` show ?thesis ``` wenzelm@45005 ` 158` ``` apply (rule ring_hom_cringI) ``` wenzelm@45005 ` 159` ``` apply (rule rcos_ring_hom_ring) ``` wenzelm@45005 ` 160` ``` apply (rule is_cring) ``` wenzelm@45005 ` 161` ``` apply (rule quotient_is_cring) ``` wenzelm@45005 ` 162` ``` apply (rule is_cring) ``` wenzelm@45005 ` 163` ``` done ``` ballarin@27611 ` 164` ```qed ``` ballarin@20318 ` 165` wenzelm@35849 ` 166` ballarin@20318 ` 167` ```subsection {* Factorization over Prime Ideals *} ``` ballarin@20318 ` 168` ballarin@20318 ` 169` ```text {* The quotient ring generated by a prime ideal is a domain *} ``` wenzelm@45005 ` 170` ```lemma (in primeideal) quotient_is_domain: "domain (R Quot I)" ``` wenzelm@45005 ` 171` ``` apply (rule domain.intro) ``` wenzelm@45005 ` 172` ``` apply (rule quotient_is_cring, rule is_cring) ``` wenzelm@45005 ` 173` ``` apply (rule domain_axioms.intro) ``` wenzelm@45005 ` 174` ``` apply (simp add: FactRing_def) defer 1 ``` wenzelm@45005 ` 175` ``` apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarify) ``` wenzelm@45005 ` 176` ``` apply (simp add: rcoset_mult_add) defer 1 ``` ballarin@20318 ` 177` ```proof (rule ccontr, clarsimp) ``` ballarin@20318 ` 178` ``` assume "I +> \ = I" ``` wenzelm@45005 ` 179` ``` then have "\ \ I" by (simp only: a_coset_join1 one_closed a_subgroup) ``` wenzelm@45005 ` 180` ``` then have "carrier R \ I" by (subst one_imp_carrier, simp, fast) ``` wenzelm@45005 ` 181` ``` with a_subset have "I = carrier R" by fast ``` wenzelm@45005 ` 182` ``` with I_notcarr show False by fast ``` ballarin@20318 ` 183` ```next ``` ballarin@20318 ` 184` ``` fix x y ``` ballarin@20318 ` 185` ``` assume carr: "x \ carrier R" "y \ carrier R" ``` wenzelm@45005 ` 186` ``` and a: "I +> x \ y = I" ``` wenzelm@45005 ` 187` ``` and b: "I +> y \ I" ``` ballarin@20318 ` 188` ballarin@20318 ` 189` ``` have ynI: "y \ I" ``` ballarin@20318 ` 190` ``` proof (rule ccontr, simp) ``` ballarin@20318 ` 191` ``` assume "y \ I" ``` wenzelm@45005 ` 192` ``` then have "I +> y = I" by (rule a_rcos_const) ``` wenzelm@45005 ` 193` ``` with b show False by simp ``` ballarin@20318 ` 194` ``` qed ``` ballarin@20318 ` 195` wenzelm@45005 ` 196` ``` from carr have "x \ y \ I +> x \ y" by (simp add: a_rcos_self) ``` wenzelm@45005 ` 197` ``` then have xyI: "x \ y \ I" by (simp add: a) ``` ballarin@20318 ` 198` wenzelm@45005 ` 199` ``` from xyI and carr have xI: "x \ I \ y \ I" by (simp add: I_prime) ``` wenzelm@45005 ` 200` ``` with ynI have "x \ I" by fast ``` wenzelm@45005 ` 201` ``` then show "I +> x = I" by (rule a_rcos_const) ``` ballarin@20318 ` 202` ```qed ``` ballarin@20318 ` 203` ballarin@20318 ` 204` ```text {* Generating right cosets of a prime ideal is a homomorphism ``` ballarin@20318 ` 205` ``` on commutative rings *} ``` wenzelm@45005 ` 206` ```lemma (in primeideal) rcos_ring_hom_cring: "ring_hom_cring R (R Quot I) (op +> I)" ``` wenzelm@45005 ` 207` ``` by (rule rcos_ring_hom_cring) (rule is_cring) ``` ballarin@20318 ` 208` ballarin@20318 ` 209` ballarin@20318 ` 210` ```subsection {* Factorization over Maximal Ideals *} ``` ballarin@20318 ` 211` ballarin@20318 ` 212` ```text {* In a commutative ring, the quotient ring over a maximal ideal ``` ballarin@20318 ` 213` ``` is a field. ``` ballarin@20318 ` 214` ``` The proof follows ``W. Adkins, S. Weintraub: Algebra -- ``` ballarin@20318 ` 215` ``` An Approach via Module Theory'' *} ``` ballarin@20318 ` 216` ```lemma (in maximalideal) quotient_is_field: ``` ballarin@27611 ` 217` ``` assumes "cring R" ``` ballarin@20318 ` 218` ``` shows "field (R Quot I)" ``` ballarin@27611 ` 219` ```proof - ``` ballarin@29237 ` 220` ``` interpret cring R by fact ``` wenzelm@45005 ` 221` ``` show ?thesis ``` wenzelm@45005 ` 222` ``` apply (intro cring.cring_fieldI2) ``` wenzelm@45005 ` 223` ``` apply (rule quotient_is_cring, rule is_cring) ``` wenzelm@45005 ` 224` ``` defer 1 ``` wenzelm@45005 ` 225` ``` apply (simp add: FactRing_def A_RCOSETS_defs a_r_coset_def[symmetric], clarsimp) ``` wenzelm@45005 ` 226` ``` apply (simp add: rcoset_mult_add) defer 1 ``` wenzelm@45005 ` 227` ``` proof (rule ccontr, simp) ``` wenzelm@45005 ` 228` ``` --{* Quotient is not empty *} ``` wenzelm@45005 ` 229` ``` assume "\\<^bsub>R Quot I\<^esub> = \\<^bsub>R Quot I\<^esub>" ``` wenzelm@45005 ` 230` ``` then have II1: "I = I +> \" by (simp add: FactRing_def) ``` wenzelm@45005 ` 231` ``` from a_rcos_self[OF one_closed] have "\ \ I" ``` wenzelm@45005 ` 232` ``` by (simp add: II1[symmetric]) ``` wenzelm@45005 ` 233` ``` then have "I = carrier R" by (rule one_imp_carrier) ``` wenzelm@45005 ` 234` ``` with I_notcarr show False by simp ``` wenzelm@45005 ` 235` ``` next ``` wenzelm@45005 ` 236` ``` --{* Existence of Inverse *} ``` wenzelm@45005 ` 237` ``` fix a ``` wenzelm@45005 ` 238` ``` assume IanI: "I +> a \ I" and acarr: "a \ carrier R" ``` ballarin@20318 ` 239` wenzelm@45005 ` 240` ``` --{* Helper ideal @{text "J"} *} ``` wenzelm@45005 ` 241` ``` def J \ "(carrier R #> a) <+> I :: 'a set" ``` wenzelm@45005 ` 242` ``` have idealJ: "ideal J R" ``` wenzelm@45005 ` 243` ``` apply (unfold J_def, rule add_ideals) ``` wenzelm@45005 ` 244` ``` apply (simp only: cgenideal_eq_rcos[symmetric], rule cgenideal_ideal, rule acarr) ``` wenzelm@45005 ` 245` ``` apply (rule is_ideal) ``` wenzelm@45005 ` 246` ``` done ``` ballarin@20318 ` 247` wenzelm@45005 ` 248` ``` --{* Showing @{term "J"} not smaller than @{term "I"} *} ``` wenzelm@45005 ` 249` ``` have IinJ: "I \ J" ``` wenzelm@45005 ` 250` ``` proof (rule, simp add: J_def r_coset_def set_add_defs) ``` wenzelm@45005 ` 251` ``` fix x ``` wenzelm@45005 ` 252` ``` assume xI: "x \ I" ``` wenzelm@45005 ` 253` ``` have Zcarr: "\ \ carrier R" by fast ``` wenzelm@45005 ` 254` ``` from xI[THEN a_Hcarr] acarr ``` wenzelm@45005 ` 255` ``` have "x = \ \ a \ x" by algebra ``` wenzelm@45005 ` 256` ``` with Zcarr and xI show "\xa\carrier R. \k\I. x = xa \ a \ k" by fast ``` wenzelm@45005 ` 257` ``` qed ``` ballarin@20318 ` 258` wenzelm@45005 ` 259` ``` --{* Showing @{term "J \ I"} *} ``` wenzelm@45005 ` 260` ``` have anI: "a \ I" ``` wenzelm@45005 ` 261` ``` proof (rule ccontr, simp) ``` wenzelm@45005 ` 262` ``` assume "a \ I" ``` wenzelm@45005 ` 263` ``` then have "I +> a = I" by (rule a_rcos_const) ``` wenzelm@45005 ` 264` ``` with IanI show False by simp ``` wenzelm@45005 ` 265` ``` qed ``` ballarin@20318 ` 266` wenzelm@45005 ` 267` ``` have aJ: "a \ J" ``` wenzelm@45005 ` 268` ``` proof (simp add: J_def r_coset_def set_add_defs) ``` wenzelm@45005 ` 269` ``` from acarr ``` wenzelm@45005 ` 270` ``` have "a = \ \ a \ \" by algebra ``` wenzelm@45005 ` 271` ``` with one_closed and additive_subgroup.zero_closed[OF is_additive_subgroup] ``` wenzelm@45005 ` 272` ``` show "\x\carrier R. \k\I. a = x \ a \ k" by fast ``` wenzelm@45005 ` 273` ``` qed ``` ballarin@20318 ` 274` wenzelm@45005 ` 275` ``` from aJ and anI have JnI: "J \ I" by fast ``` ballarin@20318 ` 276` wenzelm@45005 ` 277` ``` --{* Deducing @{term "J = carrier R"} because @{term "I"} is maximal *} ``` wenzelm@45005 ` 278` ``` from idealJ and IinJ have "J = I \ J = carrier R" ``` wenzelm@45005 ` 279` ``` proof (rule I_maximal, unfold J_def) ``` wenzelm@45005 ` 280` ``` have "carrier R #> a \ carrier R" ``` wenzelm@45005 ` 281` ``` using subset_refl acarr by (rule r_coset_subset_G) ``` wenzelm@45005 ` 282` ``` then show "carrier R #> a <+> I \ carrier R" ``` wenzelm@45005 ` 283` ``` using a_subset by (rule set_add_closed) ``` wenzelm@45005 ` 284` ``` qed ``` wenzelm@45005 ` 285` wenzelm@45005 ` 286` ``` with JnI have Jcarr: "J = carrier R" by simp ``` ballarin@20318 ` 287` wenzelm@45005 ` 288` ``` --{* Calculating an inverse for @{term "a"} *} ``` wenzelm@45005 ` 289` ``` from one_closed[folded Jcarr] ``` wenzelm@45005 ` 290` ``` have "\r\carrier R. \i\I. \ = r \ a \ i" ``` wenzelm@45005 ` 291` ``` by (simp add: J_def r_coset_def set_add_defs) ``` wenzelm@45005 ` 292` ``` then obtain r i where rcarr: "r \ carrier R" ``` wenzelm@45005 ` 293` ``` and iI: "i \ I" and one: "\ = r \ a \ i" by fast ``` wenzelm@45005 ` 294` ``` from one and rcarr and acarr and iI[THEN a_Hcarr] ``` wenzelm@45005 ` 295` ``` have rai1: "a \ r = \i \ \" by algebra ``` ballarin@20318 ` 296` wenzelm@45005 ` 297` ``` --{* Lifting to cosets *} ``` wenzelm@45005 ` 298` ``` from iI have "\i \ \ \ I +> \" ``` wenzelm@45005 ` 299` ``` by (intro a_rcosI, simp, intro a_subset, simp) ``` wenzelm@45005 ` 300` ``` with rai1 have "a \ r \ I +> \" by simp ``` wenzelm@45005 ` 301` ``` then have "I +> \ = I +> a \ r" ``` wenzelm@45005 ` 302` ``` by (rule a_repr_independence, simp) (rule a_subgroup) ``` wenzelm@45005 ` 303` wenzelm@45005 ` 304` ``` from rcarr and this[symmetric] ``` wenzelm@45005 ` 305` ``` show "\r\carrier R. I +> a \ r = I +> \" by fast ``` wenzelm@45005 ` 306` ``` qed ``` ballarin@27611 ` 307` ```qed ``` ballarin@20318 ` 308` ballarin@20318 ` 309` ```end ```