Documentation Verification Report

Nonunits

📁 Source: Mathlib/RingTheory/Ideal/Nonunits.lean

Statistics

Metric	Count
Definitions `nonunits`	1
Theorems `inv_mem_of_isUnit`, `isUnit_iff`, `isUnit_iff_and`, `isUnit_iff_of_ne_zero`, `mem_nonunits_iff`, `mem_nonunits_iff_of_ne_zero`, `mem_nonunits_iff_or`, `coe_subset_nonunits`, `exists_max_ideal_of_mem_nonunits`, `map_mem_nonunits_iff`, `mem_nonunits_iff`, `mul_mem_nonunits_left`, `mul_mem_nonunits_right`, `one_notMem_nonunits`, `zero_mem_nonunits`	15
Total	16

Submonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inv_mem_of_isUnit` 📖	mathematical	`IsUnit` `SetLike.instMembership` `SubmonoidClass.toMonoid` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`map_inv` `MonoidHom.instMonoidHomClass`
`isUnit_iff` 📖	mathematical	—	`IsUnit` `SetLike.instMembership` `SubmonoidClass.toMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`inv_mem_of_isUnit` `mul_inv_cancel` `inv_mul_cancel`
`isUnit_iff_and` 📖	mathematical	—	`IsUnit` `SetLike.instMembership` `SubmonoidClass.toMonoid` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`IsUnit.ne_zero` `GroupWithZero.toNontrivial` `IsUnit.map` `MonoidHom.instMonoidHomClass` `inv_mem_of_isUnit` `mul_inv_cancel₀` `inv_mul_cancel₀`
`isUnit_iff_of_ne_zero` 📖	mathematical	—	`IsUnit` `SetLike.instMembership` `SubmonoidClass.toMonoid` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`isUnit_iff_and`
`mem_nonunits_iff` 📖	mathematical	—	`SetLike.instMembership` `Set` `Set.instMembership` `nonunits` `SubmonoidClass.toMonoid` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mem_nonunits_iff` `isUnit_iff`
`mem_nonunits_iff_of_ne_zero` 📖	mathematical	—	`SetLike.instMembership` `Set` `Set.instMembership` `nonunits` `SubmonoidClass.toMonoid` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`mem_nonunits_iff_or`
`mem_nonunits_iff_or` 📖	mathematical	—	`SetLike.instMembership` `Set` `Set.instMembership` `nonunits` `SubmonoidClass.toMonoid` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`mem_nonunits_iff` `isUnit_iff_and` `not_and_or`

(root)

Definitions

Name	Category	Theorems
`nonunits` 📖	CompOp	15 math math: `smoothSheafCommRing.nonunits_stalk`, `mem_nonunits_iff`, `IsLocalRing.mem_maximalIdeal`, `Submonoid.mem_nonunits_iff`, `nonunits.isClosed`, `nonunits.subset_compl_ball`, `coe_subset_nonunits`, `Submonoid.mem_nonunits_iff_or`, `map_mem_nonunits_iff`, `Ring.KrullDimLE.isNilpotent_iff_mem_nonunits`, `Submonoid.mem_nonunits_iff_of_ne_zero`, `PadicInt.p_nonunit`, `zero_mem_nonunits`, `one_notMem_nonunits`, `PadicInt.mem_nonunits`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_subset_nonunits` 📖	mathematical	—	`Set` `Set.instHasSubset` `SetLike.coe` `Ideal` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `nonunits` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Ideal.eq_top_of_isUnit_mem`
`exists_max_ideal_of_mem_nonunits` 📖	mathematical	`Set` `Set.instMembership` `nonunits` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`Ideal.IsMaximal` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Ideal.span_singleton_eq_top` `Ideal.exists_le_maximal` `Ideal.subset_span` `Set.mem_singleton`
`map_mem_nonunits_iff` 📖	mathematical	—	`Set` `Set.instMembership` `nonunits` `DFunLike.coe`	—	`IsUnit.map` `IsUnit.of_map`
`mem_nonunits_iff` 📖	mathematical	—	`Set` `Set.instMembership` `nonunits` `IsUnit`	—	—
`mul_mem_nonunits_left` 📖	mathematical	`Set` `Set.instMembership` `nonunits` `CommMonoid.toMonoid`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`isUnit_of_mul_isUnit_left` `instIsDedekindFiniteMonoid`
`mul_mem_nonunits_right` 📖	mathematical	`Set` `Set.instMembership` `nonunits` `CommMonoid.toMonoid`	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`isUnit_of_mul_isUnit_right` `instIsDedekindFiniteMonoid`
`one_notMem_nonunits` 📖	mathematical	—	`Set` `Set.instMembership` `nonunits` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`isUnit_one`
`zero_mem_nonunits` 📖	mathematical	—	`Set` `Set.instMembership` `nonunits` `MonoidWithZero.toMonoid` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass`	—	`isUnit_zero_iff`

---

← Back to Index