Theorems · Theorem · number theory
Zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero
∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d] {a b : ℤ√↑d}, a * b = 0 → a = 0 ∨ b = 0- Defined in
- Mathlib.NumberTheory.Zsqrtd.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 39 from the axioms · uses propext, Quot.sound
- Assumes
- Zsqrtd.Nonsquare
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- mul_assocproof · cited by 1,667
- neg_negproof · cited by 960
- neg_mulproof · cited by 654
- mul_negproof · cited by 590
- mul_left_commproof · cited by 184
- Zsqrtdstatement and proof · cited by 105
- Zsqrtd.improof · cited by 54
- Zsqrtd.reproof · cited by 53
- mul_right_cancel₀proof · cited by 22
- eq_neg_of_add_eq_zero_leftproof · cited by 21
- Zsqrtd.Nonsquarestatement and proof · cited by 12
- Zsqrtd.mk.noConfusionproof · cited by 5
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.