Def NonUnitalSubring.toSubsemigroup

Modification history

2024-11-04 05:25

Mathlib/RingTheory/NonUnitalSubring/Basic.lean

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

Modified NonUnitalSubring.toSubsemigroup View on Github →

2023-07-01 15:01

Mathlib/RingTheory/NonUnitalSubring/Basic.lean

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

Added NonUnitalSubring.toSubsemigroup View on Github →