Added the definitions of :-

- An Intergal Domains
- An Euclidean Norm over an Integral Domain
- An Euclidean Domain

Added a file called Module.idr and added

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

- 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)
- Provided the definitions of a Common Factor Type and a GCD Type. (I did not prove that such a GCD would be unique)
- Proved the following facts about the GCD (This had about 4 auxiliary proofs): (Which was also later improved upon by other people)
- If d is a GCD of a and b, then d is also a GCD of a + b and b.
- If d is a GCD of a + b and b, then d is also a GCD of a and b.
- If d is a GCD of a and b, then d is also a GCD of b and a.

```
commit e5b8b2db46834ed2328c1085d65485c507968b49
Author: rohit3499 <47004225+rohit3499@users.noreply.github.com>
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
Author: rohit3499 <47004225+rohit3499@users.noreply.github.com>
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
Author: rohit3499 <47004225+rohit3499@users.noreply.github.com>
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
Author: rohit3499 <47004225+rohit3499@users.noreply.github.com>
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
Author: rohit3499 <47004225+rohit3499@users.noreply.github.com>
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
Author: rohit3499 <47004225+rohit3499@users.noreply.github.com>
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(+)
commit c8ad0d45487523d6ad5fa570750350a7fcec07d3
Author: rohit3499 <47004225+rohit3499@users.noreply.github.com>
AuthorDate: Mon Feb 11 01:27:40 2019 +0530
Commit: GitHub
CommitDate: Mon Feb 11 01:27:40 2019 +0530
Add files via upload
bezout.idr | 204 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 204 insertions(+)
commit 260b1e8ba1453a79e1c54f120656a8ae870546e7
Author: rohit3499 <47004225+rohit3499@users.noreply.github.com>
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
Author: rohit3499 <47004225+rohit3499@users.noreply.github.com>
AuthorDate: Tue Jan 29 22:19:50 2019 +0530
Commit: GitHub
CommitDate: Tue Jan 29 22:19:50 2019 +0530
Euclid's division lemma with proof
Provided a partial proof for Euclid's Division Lemma. Given a and b, there exist (not necessarily unique at this point) a quotient and remainder.
Code/Bezout.idr | 98 +++++++++++++++++++++++++++++++++++++++++++++++++++------
1 file changed, 89 insertions(+), 9 deletions(-)