Theorem RCLike.conj_nat_cast

Modification history

2026-10-23 15:44

Mathlib/Analysis/RCLike/Basic.lean

chore: rename `coe_nat`/`nat_cast` lemmas to `natCast` (#44825) …

Deleted RCLike.conj_nat_cast View on Github →

2024-03-29 22:03

Mathlib/Analysis/RCLike/Basic.lean

chore: remove Complex/RCLike bit0/1 lemmas (#11414) …

Added RCLike.conj_nat_cast View on Github →