Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison BAlgbra.agda @ 423:9984cdd88da3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 01 Aug 2020 18:05:23 +0900
parents 44a484f17f26
children cc7909f86841
comparison
equal deleted inserted replaced
422:44a484f17f26 423:9984cdd88da3
92 field 92 field
93 +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c 93 +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c
94 x-assoc : {a b c : L } → a x ( b x c ) ≡ (a x b) x c 94 x-assoc : {a b c : L } → a x ( b x c ) ≡ (a x b) x c
95 +-sym : {a b : L } → a + b ≡ b + a 95 +-sym : {a b : L } → a + b ≡ b + a
96 -sym : {a b : L } → a x b ≡ b x a 96 -sym : {a b : L } → a x b ≡ b x a
97 -aab : {a b : L } → a + ( a x b ) ≡ a 97 +-aab : {a b : L } → a + ( a x b ) ≡ a
98 x-aab : {a b : L } → a x ( a + b ) ≡ a 98 x-aab : {a b : L } → a x ( a + b ) ≡ a
99 -dist : {a b c : L } → a + ( b x c ) ≡ ( a x b ) + ( a x c ) 99 +-dist : {a b c : L } → a + ( b x c ) ≡ ( a x b ) + ( a x c )
100 x-dist : {a b c : L } → a x ( b + c ) ≡ ( a + b ) x ( a + c ) 100 x-dist : {a b c : L } → a x ( b + c ) ≡ ( a + b ) x ( a + c )
101 a+0 : {a : L } → a + b0 ≡ a 101 a+0 : {a : L } → a + b0 ≡ a
102 ax1 : {a : L } → a x b1 ≡ a 102 ax1 : {a : L } → a x b1 ≡ a
103 a+-a1 : {a : L } → a + ( - a ) ≡ b1 103 a+-a1 : {a : L } → a + ( - a ) ≡ b1
104 ax-a0 : {a : L } → a x ( - a ) ≡ b0 104 ax-a0 : {a : L } → a x ( - a ) ≡ b0