Theorem Complex.abs_add_eq

Modification history

2025-02-24 10:06

Mathlib/Analysis/Complex/Arg.lean

chore(Data/Complex): deprecate `Complex.abs` (#21995) …

Deleted Complex.abs_add_eq View on Github →

2023-05-25 23:22

Mathlib/Analysis/Complex/Arg.lean

feat: port Analysis.Complex.Arg (#4355)

Added Complex.abs_add_eq View on Github →