Theorems · Theorem · several complex variables
UpperHalfPlane.mul_eq_zero_iff
∀ {f g : UpperHalfPlane → ℂ}, MDiff f → MDiff g → (f * g = 0 ↔ f = 0 ∨ g = 0)- Cited by
- 0 results in Mathlib
- Foundations
- Depth 288 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement and proof · cited by 5,565
- modelWithCornersSelfstatement and proof · cited by 920
- UpperHalfPlanestatement and proof · cited by 626
- MDifferentiablestatement and proof · cited by 134
- Filter.Frequently.of_forallproof · cited by 25
- Filter.frequently_or_distribproof · cited by 2
- UpperHalfPlane.eq_zero_of_frequentlyproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.