Mathlib Map

Theorems · Definition · commutative algebra

nonunits

(α : Type u_4) → [Monoid α] → Set α

The set of non-invertible elements of a monoid.

Defined in
Mathlib.RingTheory.Ideal.Nonunits
Cited by
35 results in Mathlib
Foundations
Depth 4 from the axioms · uses no axioms
Assumes
Monoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

IsLocalization.AtPrime.isLocalRing · cited by 19AtPrime.isLocalRingmem_nonunits_iff · cited by 7mem_nonunits_iffIsLocalRing.mem_maximalIdeal · cited by 6IsLocalRing.mem_maximalId…IsLocalRing.of_unique_max_ideal · cited by 4IsLocalRing.of_unique_max…isCoprime_of_dvd · cited by 4isCoprime_of_dvdexists_max_ideal_of_mem_nonunits · cited by 3exists_max_ideal_of_mem_n…PadicInt.mem_nonunits · cited by 3PadicInt.mem_nonunitsEuclideanDomain.isCoprime_of_dvd · cited by 2EuclideanDomain.isCoprime…nonunits.isClosed · cited by 2nonunits.isClosedcoe_subset_nonunits · cited by 2coe_subset_nonunitsIsLocalRing.of_nonunits_add · cited by 2IsLocalRing.of_nonunits_a…Polynomial.separable_iff_derivative_ne_zero · cited by 2Polynomial.separable_iff_…Ideal.closure_ne_top · cited by 1Ideal.closure_ne_topPadicInt.p_nonunit · cited by 1PadicInt.p_nonunitdivRadical_dvd_derivative · cited by 1divRadical_dvd_derivativeSet · cited by 53352SetSet.ofPred · cited by 6101Set.ofPredMonoid · cited by 3887MonoidIsUnit · cited by 1602IsUnitnonunitsCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Setstatement · cited by 53,352
  • Set.ofPredproof · cited by 6,101
  • Monoidstatement and proof · cited by 3,887
  • IsUnitproof · cited by 1,602

Cited by36

Results whose statement or proof uses this declaration.