Def Subring.ofClass

Modification history

2026-03-24 12:02

Mathlib/Algebra/Ring/Subring/Defs.lean

feat(Algebra/Ring/Subring): drop associativity condition for `Subring`s (#36735) …

Modified Subring.ofClass View on Github →

2025-04-10 05:14

Mathlib/Algebra/Ring/Subring/Defs.lean

feat: `def ofClass` and `CanLift` instances for algebraic subobjects (#23708) …

Added Subring.ofClass View on Github →