Theorem RCLike.reCLM_norm

Modification history

2025-08-22 20:24

Mathlib/Analysis/RCLike/Lemmas.lean

refactor: Use `StrongDual` (#28726) …

Modified RCLike.reCLM_norm View on Github →

2024-03-28 10:26

Mathlib/Data/RCLike/Lemmas.lean

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

Added RCLike.reCLM_norm View on Github →