issues
search
SKolodynski
/
IsarMathLib
IsarMathLib is a library of formalized mathematics for Isabelle/ZF.
https://isarmathlib.org
Other
17
stars
2
forks
source link
Ring ideals
#24
Open
dan323
opened
1 year ago
dan323
commented
1 year ago
I am adding some results on rings:
[x] Ring ideal definition
[x] Product and sum of ideals
[x] Prime ideal definition
[x] Maximal ideal definition
[x] Spectrum and Zariski topology
[x] Ring homomorphism
[x] Quotient of ring by ideal
[ ] Integral domain definition
[ ] PID definition
[ ] Euclidean ring definition
[ ] Ideal maximal in commutative ring iff quotient field
[x] Ideal prime in commutative ring iff quotient integral domain
[ ] Ring of polynomials
[x] Ring modules
dan323
commented
1 year ago
First part on MR #23
I am adding some results on rings: