Mathlib Map

Theorems · Definition · group theory

Units.inv

{α : Type u} → [inst : Monoid α] → αˣ → α

The inverse value of val in the base Monoid.

Defined in
Mathlib.Algebra.Group.Units.Defs
Cited by
35 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
Monoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Units.map · cited by 95Units.mapModule.End.isUnit_iff · cited by 21End.isUnit_iffisUnit_iff_exists · cited by 12isUnit_iff_existsLinearMap.GeneralLinearGroup.toLinearEquiv · cited by 9GeneralLinearGroup.toLine…Units.inv_val · cited by 8Units.inv_valUnits.val_inv · cited by 8Units.val_invHahnSeries.toOrderTopSubOnePos · cited by 5HahnSeries.toOrderTopSubO…MulEquiv.piUnits · cited by 5MulEquiv.piUnitsspectrum.unit_mem_mul_comm · cited by 3spectrum.unit_mem_mul_commLeftCancelMonoid.eq_one_of_mul_right · cited by 3LeftCancelMonoid.eq_one_o…IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow · cited by 3Rat.isIntegralClosure_adj…Module.End.isUnit_apply_inv_apply_of_isUnit · cited by 3End.isUnit_apply_inv_appl…analyticAt_inverse · cited by 3analyticAt_inverseisField_of_isIntegral_of_isField' · cited by 3isField_of_isIntegral_of_…FractionalIdeal.eq_one_div_of_mul_eq_one_right · cited by 3FractionalIdeal.eq_one_di…Monoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.invCITED BYCITES

Cites2

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

Cited by41

Results whose statement or proof uses this declaration.