From 52ce107a04ab329e433f39d9c91aa19efde2c95f Mon Sep 17 00:00:00 2001 From: William Ball Date: Sun, 12 Jan 2025 21:03:06 -0800 Subject: [PATCH] cleaned up algebra, getting ready for more updates --- examples/algebra.pg | 6 ------ 1 file changed, 6 deletions(-) diff --git a/examples/algebra.pg b/examples/algebra.pg index a2785a7..7073ebb 100644 --- a/examples/algebra.pg +++ b/examples/algebra.pg @@ -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 := #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 := eq_sym G a (i (i a)) (right_inv_unique (i a) a (inv_lG a));