Documentation Verification Report

Basic

📁 Source: Mathlib/RingTheory/LocalRing/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `instIsLocalRing`, `isUnit_of_mem_nonunits_one_sub_self`, `isUnit_one_sub_self_of_mem_nonunits`, `isUnit_or_isUnit_of_isUnit_add`, `isUnit_or_isUnit_one_sub_self`, `nonunits_add`, `of_isUnit_or_isUnit_of_isUnit_add`, `of_isUnit_or_isUnit_one_sub_self`, `of_nonunits_add`, `of_surjective'`, `of_unique_max_ideal`, `of_unique_nonzero_prime`	12
Total	12

Field

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsLocalRing` 📖	mathematical	—	`IsLocalRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `toSemifield`	—	`IsLocalRing.of_isUnit_or_isUnit_one_sub_self` `DivisionRing.toNontrivial` `sub_zero` `isUnit_one`

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isUnit_of_mem_nonunits_one_sub_self` 📖	mathematical	`Set` `Set.instMembership` `nonunits` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	`IsUnit`	—	`isUnit_or_isUnit_one_sub_self`
`isUnit_one_sub_self_of_mem_nonunits` 📖	mathematical	`Set` `Set.instMembership` `nonunits` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`IsUnit` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`isUnit_or_isUnit_one_sub_self`
`isUnit_or_isUnit_of_isUnit_add` 📖	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—	`isUnit_of_mul_isUnit_right` `instIsDedekindFiniteMonoid` `isUnit_or_isUnit_of_add_one` `mul_add` `Distrib.leftDistribClass` `Units.inv_mul_eq_one`
`isUnit_or_isUnit_one_sub_self` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	—	`isUnit_or_isUnit_of_isUnit_add` `isUnit_one` `add_sub_cancel`
`nonunits_add` 📖	mathematical	`Set` `Set.instMembership` `nonunits` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isUnit_or_isUnit_of_isUnit_add`
`of_isUnit_or_isUnit_of_isUnit_add` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`IsLocalRing`	—	`isUnit_one`
`of_isUnit_or_isUnit_one_sub_self` 📖	mathematical	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne`	`IsLocalRing`	—	`add_sub_cancel_left`
`of_nonunits_add` 📖	mathematical	`Set` `Set.instMembership` `nonunits` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	`IsLocalRing`	—	`or_iff_not_and_not` `isUnit_one`
`of_surjective'` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ring.toSemiring` `RingHom.instFunLike`	`IsLocalRing`	—	`of_isUnit_or_isUnit_one_sub_self` `RingHom.isUnit_map` `isUnit_or_isUnit_one_sub_self` `RingHom.map_one` `RingHom.map_sub`
`of_unique_max_ideal` 📖	mathematical	`ExistsUnique` `Ideal` `CommSemiring.toSemiring` `Ideal.IsMaximal`	`IsLocalRing`	—	`of_nonunits_add` `nontrivial_of_ne` `Ideal.IsMaximal.out` `Ideal.eq_top_iff_one` `Ideal.zero_mem` `exists_max_ideal_of_mem_nonunits` `Ideal.eq_top_of_isUnit_mem` `Ideal.add_mem`
`of_unique_nonzero_prime` 📖	mathematical	`ExistsUnique` `Ideal` `CommSemiring.toSemiring` `Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.IsPrime`	`IsLocalRing`	—	`of_unique_max_ideal` `Ideal.maximal_of_no_maximal` `ne_of_lt` `ne_bot_of_gt` `Ideal.IsMaximal.isPrime` `Ideal.IsMaximal.out` `bot_lt_iff_ne_bot`

---

← Back to Index