Theorems · Theorem · group theory
div_ne_zero
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, a ≠ 0 → b ≠ 0 → a / b ≠ 0- Cited by
- 29 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- GroupWithZero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- div_eq_mul_invproof · cited by 715
- GroupWithZerostatement and proof · cited by 691
- mul_ne_zeroproof · cited by 178
- inv_ne_zeroproof · cited by 99
Cited by29
Results whose statement or proof uses this declaration.
- Real.log_divproof · cited by 21
- Real.Angle.neg_pi_div_two_ne_zeroproof · cited by 6
- Real.Angle.pi_div_two_ne_zeroproof · cited by 6
- Complex.Gamma_ne_zeroproof · cited by 6
- Complex.canonicalFactor_ne_zeroproof · cited by 6
- Complex.angle_eq_abs_argproof · cited by 4
- Complex.Gamma_mul_Gamma_one_subproof · cited by 3
- Function.Periodic.differentiableAt_cuspFunctionproof · cited by 2
- integral_gaussian_complexproof · cited by 2
- WeierstrassCurve.Projective.dblU_ne_zero_of_Y_eqproof · cited by 1
- UpperHalfPlane.deriv_smul_ne_zeroproof · cited by 1
- Real.doublingGamma_add_oneproof · cited by 1