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

right inverse unique

Browse source
This commit is contained in:
William Ball 2024-12-06 16:30:44 -08:00
parent 310c144b76
commit 832af2271f
1 changed files with 30 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
examples/algebra.pg
View file

@ -161,4 +161,34 @@ section Group
-- e * a^-1 = a^-1
(id_lg (i a)))));
-- And so are right inverses
def right_inv_unique (a b : G) (h : right_inverse a b) : eq G b (i a) :=
-- b = e * b
-- = (a^-1 * a) * b
-- = a^-1 * (a * b)
-- = a^-1 * e
-- = a^-1
eq_trans G b (op e b) (i a)
-- b = e * b
(eq_sym G (op e b) b (id_lg b))
-- e * b = a^-1
(eq_trans G (op e b) (op (op (i a) a) b) (i a)
-- e * b = (a^-1 * a) * b
(eq_cong G G e (op (i a) a) (fun (x : G) => op x b)
-- e = (a^-1 * a)
(eq_sym G (op (i a) a) e (inv_lg a)))
-- (a^-1 * a) * b = a^-1
(eq_trans G (op (op (i a) a) b) (op (i a) (op a b)) (i a)
-- (a^-1 * a) * b = a^-1 * (a * b)
(eq_sym G (op (i a) (op a b)) (op (op (i a) a) b) (assoc_g (i a) a b))
-- a^-1 * (a * b) = a^-1
(eq_trans G (op (i a) (op a b)) (op (i a) e) (i a)
-- a^-1 * (a * b) = a^-1 * e
(eq_cong G G (op a b) e (op (i a)) h)
-- a^-1 * e = a^-1
(id_rg (i a)))));
end Group