Documentation Verification Report

Henselian

📁 Source: Mathlib/RingTheory/Henselian.lean

Statistics

Metric	Count
Definitions `HenselianLocalRing`, `HenselianRing`	2
Theorems `henselian`, `is_henselian`, `toIsLocalRing`, `is_henselian`, `jac`, `henselianRing`, `instHenselianRingMaximalIdeal`, `isLocalHom_of_le_jacobson_bot`	8
Total	10

Field

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`henselian` 📖	mathematical	—	`HenselianLocalRing` `toCommRing`	—	`instIsLocalRing` `Ideal.eq_bot_of_prime` `Ideal.IsMaximal.isPrime'` `IsLocalRing.maximalIdeal.isMaximal` `sub_self`

HenselianLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`is_henselian` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsLocalRing.maximalIdeal` `toIsLocalRing` `Polynomial.eval` `IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DFunLike.coe` `LinearMap` `RingHom.id` `Polynomial` `Polynomial.semiring` `Polynomial.module` `LinearMap.instFunLike` `Polynomial.derivative`	`Polynomial.IsRoot` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing`	—	—
`toIsLocalRing` 📖	mathematical	—	`IsLocalRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—

HenselianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`is_henselian` 📖	mathematical	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal` `SetLike.instMembership` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Polynomial.eval` `IsUnit` `HasQuotient.Quotient` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal.Quotient.semiring` `DFunLike.coe` `RingHom` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `RingHom.instFunLike` `LinearMap` `RingHom.id` `Polynomial` `Polynomial.semiring` `Polynomial.module` `LinearMap.instFunLike` `Polynomial.derivative`	`Polynomial.IsRoot` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	—
`jac` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.jacobson` `CommRing.toRing` `Bot.bot` `Ring.toSemiring` `Submodule.instBot`	—	—

IsAdicComplete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`henselianRing` 📖	mathematical	—	`HenselianRing`	—	`le_jacobson_bot` `Ideal.instIsTwoSided_1` `sub_eq_add_neg` `add_zero` `SModEq.add` `SModEq.zero` `Ideal.neg_mem_iff` `Ideal.mul_mem_right` `SModEq.trans` `SModEq.eval` `IsUnit.of_map` `isLocalHom_of_le_jacobson_bot` `SModEq.def` `IsScalarTower.right` `zero_add` `pow_one` `Polynomial.taylor_eval_sub` `add_neg_cancel_comm` `Polynomial.eval_eq_sum` `Nat.instAtLeastTwoHAddOfNat` `Polynomial.sum_over_range'` `MulZeroClass.zero_mul` `lt_add_of_pos_right` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `zero_lt_two` `Nat.instZeroLEOneClass` `Finset.sum_range_add_sum_Ico` `Ideal.add_mem` `one_add_one_eq_two` `Finset.sum_range_succ` `Finset.range_one` `Finset.sum_singleton` `Polynomial.taylor_coeff_zero` `Polynomial.taylor_coeff_one` `pow_zero` `mul_one` `mul_neg` `mul_left_comm` `Ring.mul_inverse_cancel` `add_neg_cancel` `Ideal.zero_mem` `Submodule.sum_mem` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Int.instIsStrictOrderedRing` `neg_neg_of_pos` `Int.instIsOrderedAddMonoid` `Mathlib.Tactic.Linarith.zero_lt_one` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `IsStrictOrderedRing.toIsOrderedRing` `Mathlib.Tactic.Linarith.natCast_nonneg` `Nat.cast_mul` `Nat.cast_add` `Nat.cast_one` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.one_mul` `mul_nonneg_of_nonpos_of_nonpos` `AddGroup.existsAddOfLE` `IsOrderedRing.toMulPosMono` `covariant_swap_add_of_covariant_add` `Int.instAddLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `Ideal.mul_mem_left` `Ideal.pow_le_pow_right` `IsScalarTower.left` `pow_mul'` `Ideal.pow_mem_pow` `Ideal.one_eq_top` `Ideal.smul_eq_mul` `SModEq.refl` `add_assoc` `SModEq.symm` `le_self_add` `Nat.instCanonicallyOrderedAdd` `IsPrecomplete.prec'` `toIsPrecomplete` `IsHausdorff.haus'` `toIsHausdorff` `SModEq.sub_mem` `SModEq.rfl`

(root)

Definitions

Name	Category	Theorems
`HenselianLocalRing` 📖	CompData	2 math math: `Field.henselian`, `HenselianLocalRing.TFAE`
`HenselianRing` 📖	CompData	2 math math: `instHenselianRingMaximalIdeal`, `IsAdicComplete.henselianRing`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHenselianRingMaximalIdeal` 📖	mathematical	—	`HenselianRing` `IsLocalRing.maximalIdeal` `CommRing.toCommSemiring` `HenselianLocalRing.toIsLocalRing`	—	`HenselianLocalRing.toIsLocalRing` `Ideal.jacobson.eq_1` `le_sInf_iff` `Eq.ge` `IsLocalRing.eq_maximalIdeal` `Ideal.instIsTwoSided_1` `HenselianLocalRing.is_henselian` `Mathlib.Tactic.Contrapose.contrapose₁` `Ideal.Quotient.eq_zero_iff_mem` `IsLocalRing.mem_maximalIdeal` `mem_nonunits_iff` `not_isUnit_zero` `IsDomain.toNontrivial` `Ideal.Quotient.isDomain` `Ideal.IsMaximal.isPrime'` `IsLocalRing.maximalIdeal.isMaximal`
`isLocalHom_of_le_jacobson_bot` 📖	mathematical	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Ideal.jacobson` `CommRing.toRing` `Bot.bot` `Ring.toSemiring` `Submodule.instBot`	`IsLocalHom` `HasQuotient.Quotient` `Ideal.instHasQuotient` `RingHom` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ideal.Quotient.semiring` `RingHom.instFunLike`	—	`Ideal.instIsTwoSided_1` `Ideal.instIsTwoSidedJacobson` `isUnit_iff_exists_inv` `instIsDedekindFiniteMonoid` `Ideal.Quotient.mk_surjective` `RingHom.map_one` `RingHom.map_mul` `Ideal.Quotient.eq` `mul_one` `sub_add_cancel` `Ideal.mem_jacobson_bot`

---

← Back to Index