/
commutative-algebra.lagda.md
32 lines (30 loc) · 1.76 KB
/
commutative-algebra.lagda.md
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
# Commutative algebra
```agda
module commutative-algebra where
open import commutative-algebra.binomial-theorem-commutative-rings public
open import commutative-algebra.binomial-theorem-commutative-semirings public
open import commutative-algebra.boolean-rings public
open import commutative-algebra.commutative-rings public
open import commutative-algebra.commutative-semirings public
open import commutative-algebra.dependent-products-commutative-rings public
open import commutative-algebra.dependent-products-commutative-semirings public
open import commutative-algebra.discrete-fields public
open import commutative-algebra.eisenstein-integers public
open import commutative-algebra.function-commutative-rings public
open import commutative-algebra.function-commutative-semirings public
open import commutative-algebra.gaussian-integers public
open import commutative-algebra.homomorphisms-commutative-rings public
open import commutative-algebra.ideals-commutative-rings public
open import commutative-algebra.integral-domains public
open import commutative-algebra.invertible-elements-commutative-rings public
open import commutative-algebra.isomorphisms-commutative-rings public
open import commutative-algebra.local-commutative-rings public
open import commutative-algebra.maximal-ideals-commutative-rings public
open import commutative-algebra.nilradical-commutative-rings public
open import commutative-algebra.powers-of-elements-commutative-rings public
open import commutative-algebra.powers-of-elements-commutative-semirings public
open import commutative-algebra.prime-ideals-commutative-rings public
open import commutative-algebra.sums-commutative-rings public
open import commutative-algebra.sums-commutative-semirings public
open import commutative-algebra.zariski-topology public
```