wball/perga
1
0
Fork 0
Code Issues 15 Pull requests Projects Releases Packages Wiki Activity Actions

cleaned up algebra, getting ready for more updates

Browse source
This commit is contained in:
William Ball 2025-01-12 21:03:06 -08:00
parent dc2a715531
commit 52ce107a04
Signed by: wball
GPG key ID: B8682D8137B70765
1 changed files with 0 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
examples/algebra.pg
View file

@ -75,12 +75,6 @@ def left_inv_unique (a b : G) (h : b * a = e) : b = i a :=
def right_inv_unique (a b : G) (h : a * b = e) : b = i a := def right_inv_unique (a b : G) (h : a * b = e) : b = i a :=
#left_inv_unique G (*>) assoc_op e id_rG id_lG i inv_lG a b h; #left_inv_unique G (*>) assoc_op e id_rG id_lG i inv_lG a b h;
def homo_preserve_inv (a : G) : f (i a) ~ j (f a) :=
#left_inv_unique H (+) assocH eH id_lH id_rH j inv_rH (f a) (f (i a))
(eq_trans H (f a * f (i a)) (f (a * i a))
)
-- WTS: f a * f (i a) ~ eH
def inverse_involutive (a : G) : i (i a) = a := def inverse_involutive (a : G) : i (i a) = a :=
eq_sym G a (i (i a)) (right_inv_unique (i a) a (inv_lG a)); eq_sym G a (i (i a)) (right_inv_unique (i a) a (inv_lG a));