Theorem RCLike.norm_ofNat

Modification history

2025-01-02 08:45

Mathlib/Analysis/RCLike/Basic.lean

chore: use `ofNat()` around `Real` and `Complex` (#20388) …

Modified RCLike.norm_ofNat View on Github →

2024-03-28 10:26

Mathlib/Data/RCLike/Basic.lean

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

Added RCLike.norm_ofNat View on Github →