## Algebra :

1. An Intergal Domains
2. An Euclidean Norm over an Integral Domain
3. An Euclidean Domain

1. The definitions of the types for distributivity of the action of the ring on the module
2. Added the definition for the IsLeftModule type
3. Added functions to recover the individual Distributivity types from the IsLeftModule type.
4. Added functions to recover the zero of the module from the IsLeftModule type
5. Proved that r.0 = 0 (Action of any ring element on zero is zero)
6. Proved that 0.m = 0 (Action of zero of the ring on any element is zero)

## Number Theory :

1. Provided a partial proof of Euclid’s Division Lemma (Existence of Quotient and Remainders when we divide a natural number by another), which was later improved upon by other people. (This also had 5 auxiliary proofs, which include Trichotomy of the order on integers and Anti-symmetry of LTE)
2. Provided the definitions of a Common Factor Type and a GCD Type. (I did not prove that such a GCD would be unique)
3. Proved the following facts about the GCD (This had about 4 auxiliary proofs): (Which was also later improved upon by other people)
1. If d is a GCD of a and b, then d is also a GCD of a + b and b.
2. If d is a GCD of a + b and b, then d is also a GCD of a and b.
3. If d is a GCD of a and b, then d is also a GCD of b and a.

### Log of git commits by author


commit e5b8b2db46834ed2328c1085d65485c507968b49
AuthorDate: Mon Apr 22 11:54:13 2019 +0530
Commit:     GitHub
CommitDate: Mon Apr 22 11:54:13 2019 +0530

Updated Report

Added my contributions after the midsems.

_reports/rohit/rohit.md | 7 +++++++
1 file changed, 7 insertions(+)

commit e25deca402b42d13d639be174cd1de7f635b380f
AuthorDate: Thu Apr 18 16:33:16 2019 +0530
Commit:     GitHub
CommitDate: Thu Apr 18 16:33:16 2019 +0530

Added a more general function extending equality

Now the function can map one type to a different type, instead of the same type

Code/NatUtils.idr | 5 +++++
1 file changed, 5 insertions(+)

commit 4acf1f296eac60ce36b79a2e8f68b6629c327055
AuthorDate: Thu Apr 18 16:29:27 2019 +0530
Commit:     GitHub
CommitDate: Thu Apr 18 16:29:27 2019 +0530

Created File Module.idr with definitions and some properties

Created the IsLeftModule type and proved some basic properties like r*0 = 0 and 0*m = 0.

Code/Module.idr | 135 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 135 insertions(+)

commit 86fdf1a3c136695ea4336bfdebe980f86138c104
AuthorDate: Mon Feb 25 01:45:48 2019 +0530
Commit:     GitHub
CommitDate: Mon Feb 25 01:45:48 2019 +0530

Updated Report

_reports/rohit/rohit.md | 18 +++++++++++++++++-
1 file changed, 17 insertions(+), 1 deletion(-)

commit 1ea453bc165ffdc61ba458e229f36968afbcc6fe
AuthorDate: Mon Feb 25 00:58:03 2019 +0530
Commit:     GitHub
CommitDate: Mon Feb 25 00:58:03 2019 +0530

Definitions of Euclidian Domains

Euclidian Norms and Euclidian Domains and also updated the definition of an Integral Domain.

Code/Ring.idr | 36 ++++++++++++++++++++++--------------
1 file changed, 22 insertions(+), 14 deletions(-)

commit 4da929e6969f7a1e549c23a0cabceaaa2850275d
AuthorDate: Sun Feb 24 18:56:10 2019 +0530
Commit:     GitHub
CommitDate: Sun Feb 24 18:56:10 2019 +0530

Added definitions for zero divisors and Integral Domains

Zero Divisors and Integral Domains

Code/Ring.idr | 11 +++++++++++
1 file changed, 11 insertions(+)

AuthorDate: Mon Feb 11 01:27:40 2019 +0530
Commit:     GitHub
CommitDate: Mon Feb 11 01:27:40 2019 +0530

bezout.idr | 204 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 204 insertions(+)

commit 260b1e8ba1453a79e1c54f120656a8ae870546e7
AuthorDate: Tue Jan 29 22:47:58 2019 +0530
Commit:     GitHub
CommitDate: Tue Jan 29 22:47:58 2019 +0530

Euclid's Division Lemma with partial proof

proved that given a and b, there exist a quotient and a remainder (not necessarily unique)

Code/Bezout.idr | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)

commit 5d44076d116d6889499d7b97a90c15ccef9ae502