Theorem RCLike.imCLM_coe

Modification history

2025-08-22 20:24

Mathlib/Analysis/RCLike/Basic.lean

refactor: Use `StrongDual` (#28726) …

Modified RCLike.imCLM_coe View on Github →

2024-03-28 10:26

Mathlib/Data/RCLike/Basic.lean

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

Added RCLike.imCLM_coe View on Github →