@@ -36,8 +36,8 @@ inverseDistributesOverGroupOp {t} l r =
36 let step11 = replace {P = \x => x = inverse r <+> inverse l} (monoidNeutralIsNeutralR (inverse (l <+> r))) step10 in
36 let step11 = replace {P = \x => x = inverse r <+> inverse l} (monoidNeutralIsNeutralR (inverse (l <+> r))) step10 in
37 replace {P = \x => inverse (l <+> r) = x} (abelianGroupOpIsCommutative (inverse r) (inverse l)) step11
37 replace {P = \x => inverse (l <+> r) = x} (abelianGroupOpIsCommutative (inverse r) (inverse l)) step11
39−multNeutralAbsorbingR : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral
39+multNeutralAbsorbingL : VerifiedRingWithUnity t => (r : t) -> A.neutral <.> r = A.neutral
40−multNeutralAbsorbingR r =
40+multNeutralAbsorbingL r =
41 let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r) in
41 let step1 = the (unity <.> r = r) (ringWithUnityIsUnityR r) in
42 let step2 = replace {P = \x => x <.> r = r} (sym $ monoidNeutralIsNeutralR unity) step1 in
42 let step2 = replace {P = \x => x <.> r = r} (sym $ monoidNeutralIsNeutralR unity) step1 in
43 let step3 = replace {P = \x => x = r} (ringOpIsDistributiveR neutral unity r) step2 in
43 let step3 = replace {P = \x => x = r} (ringOpIsDistributiveR neutral unity r) step2 in
@@ -47,8 +47,8 @@ multNeutralAbsorbingR r =
47 let step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6 in
47 let step7 = replace {P = \x => neutral <.> r <+> x = x} (groupInverseIsInverseL r) step6 in
48 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7
48 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (neutral <.> r)) step7
50−multNeutralAbsorbingL : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral
50+multNeutralAbsorbingR : VerifiedRingWithUnity t => (l : t) -> l <.> A.neutral = A.neutral
51−multNeutralAbsorbingL l =
51+multNeutralAbsorbingR l =
52 let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l) in
52 let step1 = the (l <.> unity = l) (ringWithUnityIsUnityL l) in
53 let step2 = replace {P = \x => l <.> x = l} (sym $ monoidNeutralIsNeutralR unity) step1 in
53 let step2 = replace {P = \x => l <.> x = l} (sym $ monoidNeutralIsNeutralR unity) step1 in
54 let step3 = replace {P = \x => x = l} (ringOpIsDistributiveL l neutral unity) step2 in
54 let step3 = replace {P = \x => x = l} (ringOpIsDistributiveL l neutral unity) step2 in
@@ -57,3 +57,23 @@ multNeutralAbsorbingL l =
57 let step6 = replace {P = \x => x = l <+> inverse l} (sym $ semigroupOpIsAssociative (l <.> neutral) l (inverse l)) step5 in
57 let step6 = replace {P = \x => x = l <+> inverse l} (sym $ semigroupOpIsAssociative (l <.> neutral) l (inverse l)) step5 in
58 let step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6 in
58 let step7 = replace {P = \x => l <.> neutral <+> x = x} (groupInverseIsInverseL l) step6 in
59 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7
59 replace {P = \x => x = neutral} (monoidNeutralIsNeutralL (l <.> neutral)) step7
61+multInverseInversesL : VerifiedRingWithUnity t => (l, r : t) -> inverse l <.> r = inverse (l <.> r)
62+multInverseInversesL l r =
63+ let step1 = replace {P = \x => x <.> r = neutral} (sym $ groupInverseIsInverseL l) (multNeutralAbsorbingL r) in
64+ let step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveR l (inverse l) r) step1 in
65+ let step3 = cong {f = ((inverse (l <.> r)) <+>)} step2 in
66+ let step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> inverse l <.> r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3 in
67+ let step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (inverse l <.> r)) step4 in
68+ let step6 = replace {P = \x => x <+> inverse l <.> r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5 in
69+ replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (inverse l <.> r)) step6
71+multInverseInversesR : VerifiedRingWithUnity t => (l, r : t) -> l <.> inverse r = inverse (l <.> r)
72+multInverseInversesR l r =
73+ let step1 = replace {P = \x => l <.> x = neutral} (sym $ groupInverseIsInverseL r) (multNeutralAbsorbingR l) in
74+ let step2 = replace {P = \x => x = neutral} (ringOpIsDistributiveL l r (inverse r)) step1 in
75+ let step3 = cong {f = ((inverse (l <.> r)) <+>)} step2 in
76+ let step4 = replace {P = \x => inverse (l <.> r) <+> (l <.> r <+> l <.> inverse r) = x} (monoidNeutralIsNeutralL (inverse (l <.> r))) step3 in
77+ let step5 = replace {P = \x => x = inverse (l <.> r)} (semigroupOpIsAssociative (inverse (l <.> r)) (l <.> r) (l <.> inverse r)) step4 in
78+ let step6 = replace {P = \x => x <+> l <.> inverse r = inverse (l <.> r)} (groupInverseIsInverseR (l <.> r)) step5 in
79+ replace {P = \x => x = inverse (l <.> r)} (monoidNeutralIsNeutralR (l <.> inverse r)) step6