Def RCLike.imLm

Modification history

2026-02-17 23:08

Mathlib/Analysis/RCLike/Basic.lean

chore: bump toolchain to v4.29.0-rc1 (#35459)

Deleted RCLike.imLm View on Github →

2024-03-28 10:26

Mathlib/Data/RCLike/Basic.lean

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

Added RCLike.imLm View on Github →