Commit 2026-03-24 12:02 15bbbc46

View on Github →

feat(Algebra/Ring/Subring): drop associativity condition for Subrings (#36735) cf. Item 4 in #7987.

Estimated changes

modified def RingHom.range
modified theorem Subring.card_top
modified def Subring.centralizer
modified theorem Subring.centralizer_le
modified theorem Subring.centralizer_univ
modified theorem Subring.coe_centralizer
modified def Subring.comap
modified def Subring.map
modified theorem Subring.mem_center_iff
modified theorem Subring.mem_centralizer_iff
modified theorem Subring.coe_pow
modified def Subring.ofClass
modified structure Subring