Theorems · Theorem · group theory
division_def
∀ {G : Type u_1} [inst : DivInvMonoid G] (a b : G), a / b = a * b⁻¹Alias of div_eq_mul_inv.
Dividing by an element is the same as multiplying by its inverse.
This is a duplicate of DivInvMonoid.div_eq_mul_inv ensuring that the types unfold better.
- Defined in
- Mathlib.Algebra.Group.Defs
- Cited by
- 21 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- DivInvMonoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
- DivInvMonoidstatement · cited by 103
Cited by21
Results whose statement or proof uses this declaration.
- Complex.inv_improof · cited by 13
- Complex.inv_reproof · cited by 13
- div_lt_iff_of_negproof · cited by 7
- div_neg_eq_neg_divproof · cited by 6
- Rat.cast_injectiveproof · cited by 5
- Real.sqrt_divproof · cited by 4
- inv_lt_inv_of_negproof · cited by 3
- Real.sqrt_div'proof · cited by 3
- div_nonneg_iffproof · cited by 3
- Set.preimage_mul_const_Ici₀proof · cited by 2
- Set.preimage_mul_const_Iic₀proof · cited by 2
- Set.preimage_mul_const_Iio₀proof · cited by 2