Theorem RCLike.nnnorm_ofNat

Modification history

2025-01-02 08:45

Mathlib/Analysis/RCLike/Basic.lean

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

Modified RCLike.nnnorm_ofNat View on Github →

2024-08-29 12:34

Mathlib/Analysis/RCLike/Basic.lean

feat(RCLike): `nnnorm` lemmas (#16144) …

Added RCLike.nnnorm_ofNat View on Github →