Theorems · Theorem · group theory
MulOpposite.op_div
∀ {α : Type u_1} [inst : DivInvMonoid α] (x y : α), MulOpposite.op (x / y) = (MulOpposite.op y)⁻¹ * MulOpposite.op x- Defined in
- Mathlib.Algebra.Group.Opposite
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses propext
- Assumes
- DivInvMonoid
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.
- MulOppositestatement · cited by 1,135
- div_eq_mul_invproof · cited by 715
- MulOpposite.opstatement and proof · cited by 520
- DivInvMonoidstatement and proof · cited by 103
Cited by1
Results whose statement or proof uses this declaration.
- star_div₀proof · cited by 2