Theorems · Theorem · group theory
IsUnit.val_inv_mul
∀ {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a), ↑h.unit⁻¹ * a = 1- Defined in
- Mathlib.Algebra.Group.Units.Defs
- Cited by
- 35 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses Classical.choice
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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 · cited by 2,804
- Units.valstatement · cited by 1,966
- IsUnitstatement and proof · cited by 1,602
- IsUnit.unitstatement and proof · cited by 252
- Units.mul_invproof · cited by 67
Cited by35
Results whose statement or proof uses this declaration.
- WeierstrassCurve.Jacobian.nonsingular_smulproof · cited by 5
- WeierstrassCurve.Projective.nonsingular_smulproof · cited by 5
- spectrum.unit_mem_mul_commproof · cited by 3
- IsUnit.isUnit_iff_mulRight_bijectiveproof · cited by 2
- WeierstrassCurve.Jacobian.equation_smulproof · cited by 2
- WeierstrassCurve.Projective.equation_smulproof · cited by 2
- Polynomial.isUnit_resultant_iff_isCoprimeproof · cited by 2
- Polynomial.isCoprime_X_sub_C_of_isUnit_subproof · cited by 2
- Module.IsLocalRing.linearIndependent_of_flatproof · cited by 2
- Polynomial.monic_of_isUnit_leadingCoeff_inv_smulproof · cited by 2
- LocalSubring.exists_valuationRing_of_isMaxproof · cited by 2
- MonomialOrder.sPolynomial_decompositionproof · cited by 1