Theorems · Definition · field theory
Complex.normSq
ℂ →*₀ ℝ
The norm squared function.
- Defined in
- Mathlib.Data.Complex.Basic
- Cited by
- 103 results in Mathlib
- Foundations
- Depth 105 from the axioms, rests on 1,820 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- Complexstatement and proof · cited by 5,565
- Complex.reproof · cited by 882
- MonoidWithZeroHomstatement · cited by 704
- Complex.improof · cited by 591
Cited by105
Results whose statement or proof uses this declaration.
- Complex.norm_mulproof · cited by 59
- Complex.norm_defstatement · cited by 18
- ModularGroup.fdproof · cited by 17
- Complex.norm_divproof · cited by 15
- Complex.normSq_eq_norm_sqstatement and proof · cited by 14
- Complex.normSq_nonnegstatement · cited by 14
- ModularGroup.fdoproof · cited by 13
- Complex.inv_imstatement and proof · cited by 13
- Complex.inv_restatement and proof · cited by 13
- Complex.normSq_ofRealstatement · cited by 10
- Complex.normSq_applystatement · cited by 8
- Complex.norm_conjproof · cited by 8