Theorems · Definition · group theory

Units.casesOn

{α : Type u} →
  [inst : Monoid α] →
    {motive : αˣ → Sort u_1} →
      (t : αˣ) →
        ((val inv : α) →
            (val_inv : val * inv = 1) →
              (inv_val : inv * val = 1) → motive { val := val, inv := inv, val_inv := val_inv, inv_val := inv_val }) →
          motive t

Defined in: Mathlib.Algebra.Group.Units.Defs
Cited by: 15 results in Mathlib
Foundations: Depth 8 from the axioms · uses no axioms
Assumes: Monoid

Mathlib docs Source Loogle LeanSearch

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.

Monoidstatement and proof · cited by 3,887
Unitsstatement and proof · cited by 2,804

Cited by17

Results whose statement or proof uses this declaration.

IsUnit.exists_right_invproof · cited by 11
IsUnit.exists_left_invproof · cited by 10
PowerSeries.order_zero_of_unitproof · cited by 2
IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_eqproof · cited by 1
HomogeneousLocalization.isUnit_iff_isUnit_valproof · cited by 1
IsPGroup.smul_mul_inv_trivial_or_surjectiveproof · cited by 1
IsDedekindDomain.selmerGroup.fromUnit_kerproof · cited by 1
smoothSheafCommRing.isUnit_stalk_iffproof · cited by 1
HahnSeries.isUnit_iffproof · cited by 0
Con.induction_on_unitsproof · cited by 0
Polynomial.not_isUnit_X_add_Cproof · cited by 0
StandardEtalePair.existsUnique_hasMap_of_hasMap_quotient_of_sq_eq_botproof · cited by 0