Theorems · Theorem · group theory
Units.inv_mul_eq_iff_eq_mul
∀ {α : Type u} [inst : Monoid α] (a : αˣ) {b c : α}, ↑a⁻¹ * b = c ↔ b = ↑a * c- Defined in
- Mathlib.Algebra.Group.Units.Defs
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 10 from the axioms · uses no axioms
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- Unitsstatement and proof · cited by 2,804
- Units.valstatement and proof · cited by 1,966
- Units.inv_mul_cancel_leftproof · cited by 15
- Units.mul_inv_cancel_leftproof · cited by 10
Cited by9
Results whose statement or proof uses this declaration.
- Submonoid.LocalizationMap.mul_inv_leftproof · cited by 15
- WeierstrassCurve.addSubMapCoeff_conditionproof · cited by 2
- Units.commute_iff_inv_mul_cancelproof · cited by 2
- WeierstrassCurve.ofJ1728_jproof · cited by 1
- WeierstrassCurve.ofJNe0Or1728_jproof · cited by 1
- Units.liftRight_inv_mulproof · cited by 1
- IsUnit.inv_mul_eq_iff_eq_mulproof · cited by 1
- IsLocalization.mul_add_inv_leftproof · cited by 1
- Matrix.isAdjointPair_equivproof · cited by 1