Theorem IsROrC.toOrderedSMul

Modification history

2024-03-28 10:26

Mathlib/Data/RCLike/Basic.lean

chore: Rename `IsROrC` to `RCLike` (#10819) …

Deleted IsROrC.toOrderedSMul View on Github →

2023-08-09 22:46

Mathlib/Data/IsROrC/Basic.lean

feat: IsROrC.toStarOrderedRing as a scoped instance (#6391) …

Added IsROrC.toOrderedSMul View on Github →