Def NonUnitalSubringClass.subtype

Modification history

2024-11-04 05:25

Mathlib/RingTheory/NonUnitalSubring/Basic.lean

chore(RingTheory/NonUnitalSubring): split Basic.lean (#18518) …

Modified NonUnitalSubringClass.subtype View on Github →

2023-07-01 15:01

Mathlib/RingTheory/NonUnitalSubring/Basic.lean

feat: define `NonUnitalSubring`s (#5151) …

Added NonUnitalSubringClass.subtype View on Github →