[isabelle] New AFP article: The Localization of a Commutative Ring
- To: Isabelle Users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] New AFP article: The Localization of a Commutative Ring
- From: Tobias Nipkow <nipkow at in.tum.de>
- Date: Sun, 17 Jun 2018 21:15:23 +0200
- User-agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.13; rv:52.0) Gecko/20100101 Thunderbird/52.8.0
The Localization of a Commutative Ring
We formalize the localization of a commutative ring R with respect to a
multiplicative subset (i.e. a submonoid of R seen as a multiplicative monoid).
This localization is itself a commutative ring and we build the natural
homomorphism of rings from R to its localization.
Description: S/MIME Cryptographic Signature
This archive was generated by a fusion of
Pipermail (Mailman edition) and