Documentation Verification Report

Basic

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

Statistics

Metric	Count
Definitions `equivFinTwo`, `pi`	2
Theorems `add_pow_add_pred_mem_of_pow_mem`, `add_pow_add_pred_mem_of_pow_mem_of_commute`, `add_pow_mem_of_pow_mem_of_le`, `add_pow_mem_of_pow_mem_of_le_of_commute`, `bot_lt_of_maximal`, `instFinite`, `instIsTwoSidedForallPi`, `isSimpleOrder`, `mem_pi`, `pi_le_pi_iff`, `pi_span`, `pow_multiset_sum_mem_span_pow`, `prod_mem`, `single_mem_pi`, `span_pow_eq_top`, `span_range_pow_eq_top`, `span_single_eq_top`, `sum_pow_mem_span_pow`, `exists_maximal_of_not_isField`, `exists_not_isUnit_of_not_isField`, `isField_iff_isSimpleOrder_ideal`, `isField_iff_maximal_bot`, `ne_bot_of_isMaximal_of_not_isField`, `not_isField_iff_exists_ideal_bot_lt_and_lt_top`, `not_isField_iff_exists_prime`, `not_isField_of_ne_of_ne`	26
Total	28

Ideal

Definitions

Name	Category	Theorems
`equivFinTwo` 📖	CompOp	—
`pi` 📖	CompOp	6 math math: `single_mem_pi`, `instIsTwoSidedForallPi`, `pi_le_pi_iff`, `map_evalRingHom_pi`, `pi_span`, `mem_pi`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_pow_add_pred_mem_of_pow_mem` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`add_pow_add_pred_mem_of_pow_mem_of_commute` `Commute.all`
`add_pow_add_pred_mem_of_pow_mem_of_commute` 📖	mathematical	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Distrib.toAdd`	—	`add_pow_mem_of_pow_mem_of_le_of_commute` `le_refl`
`add_pow_mem_of_pow_mem_of_le` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib`	—	`add_pow_mem_of_pow_mem_of_le_of_commute` `Commute.all`
`add_pow_mem_of_pow_mem_of_le_of_commute` 📖	mathematical	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib`	`Distrib.toAdd`	—	`Commute.add_pow` `Finset.sum_congr` `Submodule.sum_mem` `mul_mem_left` `Commute.pow_pow` `pow_mem_of_pow_mem`
`bot_lt_of_maximal` 📖	mathematical	`IsField` `CommSemiring.toSemiring`	`Ideal` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Bot.bot` `Submodule.instBot`	—	`Ne.bot_lt` `Ring.ne_bot_of_isMaximal_of_not_isField`
`instFinite` 📖	mathematical	—	`Finite` `Ideal` `DivisionSemiring.toSemiring`	—	—
`instIsTwoSidedForallPi` 📖	mathematical	`IsTwoSided`	`Pi.semiring` `pi`	—	`mul_mem_right`
`isSimpleOrder` 📖	mathematical	—	`IsSimpleOrder` `Ideal` `DivisionSemiring.toSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	—	`instNontrivial` `GroupWithZero.toNontrivial` `eq_bot_or_top`
`mem_pi` 📖	mathematical	—	`Ideal` `Pi.semiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `pi`	—	—
`pi_le_pi_iff` 📖	mathematical	—	`Ideal` `Pi.semiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `pi` `Pi.hasLe`	—	`Pi.single_eq_same` `single_mem_pi`
`pi_span` 📖	mathematical	—	`pi` `span` `Set` `Set.instSingletonSet` `Pi.semiring`	—	`ext`
`pow_multiset_sum_mem_span_pow` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `span` `SetLike.coe` `Finset` `Finset.instSetLike` `Multiset.toFinset` `Multiset.map` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Multiset.sum` `Multiset.card`	—	`Multiset.induction_on` `Finset.coe_empty` `span_empty` `MulZeroClass.zero_mul` `zero_add` `pow_one` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Multiset.map_cons` `Multiset.toFinset_cons` `Finset.coe_insert` `Multiset.sum_cons` `Multiset.card_cons` `add_pow` `Submodule.sum_mem` `mem_span_insert` `Submodule.zero_mem` `mul_comm` `pow_add` `add_zero` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `add_mul` `Distrib.rightDistribClass` `one_mul` `add_assoc` `add_comm` `add_tsub_assoc_of_le` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `mul_assoc` `mul_mem_left`
`prod_mem` 📖	mathematical	`Finset` `Finset.instMembership` `Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Finset.prod` `CommSemiring.toCommMonoid`	—	`Finset.prod_eq_prod_diff_singleton_mul` `mul_mem_left`
`single_mem_pi` 📖	mathematical	`Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Pi.semiring` `pi` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`eq_or_ne` `Pi.single_eq_same` `Pi.single_eq_of_ne'` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass`
`span_pow_eq_top` 📖	mathematical	`span` `CommSemiring.toSemiring` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Set.image` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`eq_top_iff_one` `Set.eq_empty_or_nonempty` `Set.image_empty` `subset_span` `pow_zero` `Finsupp.mem_span_iff_linearCombination` `span.eq_1` `sum_pow_mem_span_pow` `span_le` `Set.singleton_subset_iff` `Subtype.prop` `mul_pow` `mem_span_singleton` `mul_comm` `one_pow` `Finset.sum_congr`
`span_range_pow_eq_top` 📖	mathematical	`span` `CommSemiring.toSemiring` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	`Set.range` `Set.Elem` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Set` `Set.instMembership`	—	`Submodule.mem_span_finite_of_mem_span` `eq_top_iff_one` `top_unique` `LE.le.trans` `Eq.ge` `span_pow_eq_top` `span_le` `Finset.le_sup` `Finset.mem_attach` `pow_add` `mul_mem_left` `subset_span`
`span_single_eq_top` 📖	mathematical	—	`span` `Pi.semiring` `Set.range` `Pi.single` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule`	—	`eq_top_iff` `Pi.single_induction` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `add_mem` `Pi.single_eq_same` `mul_one` `mul_mem_left` `subset_span`
`sum_pow_mem_span_pow` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `span` `Set.image` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.sum` `Finset.card`	—	`Multiset.map_map` `Multiset.map_congr` `Multiset.toFinset_map` `Finset.val_toFinset` `Finset.coe_image` `Multiset.card_map` `pow_multiset_sum_mem_span_pow`

Ring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_maximal_of_not_isField` 📖	mathematical	`IsField` `CommSemiring.toSemiring`	`Ideal.IsMaximal`	—	`Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `isField_iff_maximal_bot` `bot_ne_top` `Ideal.instNontrivial` `Ideal.maximal_of_no_maximal`
`exists_not_isUnit_of_not_isField` 📖	mathematical	`IsField` `CommSemiring.toSemiring`	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`exists_pair_ne` `mul_comm` `instIsDedekindFiniteMonoid` `Mathlib.Tactic.Push.not_forall_eq`
`isField_iff_isSimpleOrder_ideal` 📖	mathematical	—	`IsField` `CommSemiring.toSemiring` `IsSimpleOrder` `Ideal` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice`	—	`subsingleton_or_nontrivial` `not_isField_of_subsingleton` `false_of_nontrivial_of_subsingleton` `IsSimpleOrder.toNontrivial` `Unique.instSubsingleton` `not_iff_not` `not_isField_iff_exists_ideal_bot_lt_and_lt_top` `Mathlib.Tactic.Contrapose.contrapose_iff₃` `Mathlib.Tactic.Push.not_and_or_eq` `Ideal.instNontrivial` `IsSimpleOrder.eq_bot_or_eq_top`
`isField_iff_maximal_bot` 📖	mathematical	—	`IsField` `CommSemiring.toSemiring` `Ideal.IsMaximal` `Bot.bot` `Ideal` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Ideal.bot_isMaximal` `exists_not_isUnit_of_not_isField` `Ideal.span_singleton_eq_bot` `Ideal.IsMaximal.eq_of_le` `Ideal.span_singleton_ne_top` `bot_le`
`ne_bot_of_isMaximal_of_not_isField` 📖	—	`IsField` `CommSemiring.toSemiring`	—	—	`not_isField_iff_exists_ideal_bot_lt_and_lt_top` `LT.lt.ne` `Ideal.IsMaximal.eq_of_le` `bot_le`
`not_isField_iff_exists_ideal_bot_lt_and_lt_top` 📖	mathematical	—	`IsField` `CommSemiring.toSemiring` `Ideal` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Bot.bot` `Submodule.instBot` `Top.top` `Submodule.instTop`	—	`exists_maximal_of_not_isField` `bot_lt_iff_ne_bot` `lt_top_iff_ne_top` `Ideal.IsMaximal.ne_top` `not_isField_of_ne_of_ne` `LT.lt.ne'` `LT.lt.ne`
`not_isField_iff_exists_prime` 📖	mathematical	—	`IsField` `CommSemiring.toSemiring` `Ideal.IsPrime`	—	`exists_maximal_of_not_isField` `Ideal.IsMaximal.isPrime` `not_isField_of_ne_of_ne` `Ideal.IsPrime.ne_top`
`not_isField_of_ne_of_ne` 📖	mathematical	—	`IsField` `CommSemiring.toSemiring`	—	`Mathlib.Tactic.Contrapose.contrapose₄` `Ideal.IsMaximal.eq_of_le` `isField_iff_maximal_bot` `bot_le`

---

← Back to Index