Commit 2023-05-14 01:40 759a5219

View on Github →

feat: port Algebra.Category.Ring.Basic (#3901) This is a replacement for https://github.com/leanprover-community/mathlib4/pull/3105 which makes use of the refactors proposed in https://github.com/leanprover-community/mathlib4/pull/3900. I'm happy to just merge this into #3105 if that's preferred, but since it depends on a refactor I thought I'd keep it separate for now.

Estimated changes

added theorem CommRingCat.coe_comp
added theorem CommRingCat.coe_id
added theorem CommRingCat.coe_of
added theorem CommRingCat.ext
added theorem CommRingCat.forget_map
added def CommRingCat.of
added def CommRingCat
added theorem CommSemiRing.coe_comp
added theorem CommSemiRing.coe_id
added theorem CommSemiRing.coe_of
added theorem CommSemiRing.ext
added def CommSemiRing.of
added def CommSemiRingCat
added theorem RingCat.coe_comp
added theorem RingCat.coe_id
added theorem RingCat.coe_of
added theorem RingCat.ext
added theorem RingCat.forget_map
added def RingCat.of
added def RingCat.ofHom
added def RingCat
added theorem SemiRingCat.coe_comp
added theorem SemiRingCat.coe_id
added theorem SemiRingCat.coe_of
added theorem SemiRingCat.ext
added theorem SemiRingCat.forget_map
added def SemiRingCat.of
added def SemiRingCat