Documentation Verification Report

TFAE

📁 Source: Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean

Statistics

Metric	Count
Definitions	0
Theorems `isPrincipalIdealRing`, `finrank_CotangentSpace_eq_one`, `finrank_CotangentSpace_eq_one_iff`, `exists_maximalIdeal_pow_eq_of_principal`, `maximalIdeal_isPrincipal_of_isDedekindDomain`, `tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain`	6
Total	6

IsDedekindDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isPrincipalIdealRing` 📖	mathematical	—	`IsPrincipalIdealRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`List.TFAE.out` `toIsDomain` `IsScalarTower.right` `tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain` `IsDedekindRing.toIsNoetherian` `toIsDedekindRing`

IsLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finrank_CotangentSpace_eq_one` 📖	mathematical	—	`Module.finrank` `ResidueField` `IsDiscreteValuationRing.toIsLocalRing` `CotangentSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `ResidueField.field` `AddCommGroup.toAddCommMonoid` `Ideal.instAddCommGroupCotangent` `maximalIdeal` `CommRing.toCommSemiring` `instModuleResidueFieldCotangentSpace`	—	`IsDiscreteValuationRing.toIsLocalRing` `finrank_CotangentSpace_eq_one_iff` `IsDedekindRing.toIsNoetherian` `IsDedekindDomain.toIsDedekindRing` `IsPrincipalIdealRing.isDedekindDomain` `IsDiscreteValuationRing.toIsPrincipalIdealRing`
`finrank_CotangentSpace_eq_one_iff` 📖	mathematical	—	`Module.finrank` `ResidueField` `CotangentSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `ResidueField.field` `AddCommGroup.toAddCommMonoid` `Ideal.instAddCommGroupCotangent` `maximalIdeal` `CommRing.toCommSemiring` `instModuleResidueFieldCotangentSpace` `IsDiscreteValuationRing`	—	`finrank_cotangentSpace_eq_zero` `IsDiscreteValuationRing.not_a_field'` `maximalIdeal_eq_bot` `List.TFAE.out` `IsScalarTower.right` `IsDiscreteValuationRing.TFAE`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_maximalIdeal_pow_eq_of_principal` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.instPowNat` `Semiring.toModule` `IsScalarTower.right` `Algebra.id` `IsLocalRing.maximalIdeal`	—	`IsScalarTower.right` `IsSimpleOrder.eq_bot_or_eq_top` `IsSimpleModule.toIsSimpleOrder` `instIsSimpleModule` `pow_zero` `Ideal.one_eq_top` `SetLike.ext_iff` `Ideal.mem_span_singleton` `Ring.ne_bot_of_isMaximal_of_not_isField` `IsLocalRing.toNontrivial` `IsLocalRing.maximalIdeal.isMaximal` `Ideal.span_singleton_zero` `IsDiscreteValuationRing.irreducible_of_span_eq_maximalIdeal` `WfDvdMonoid.not_unit_iff_exists_factors_eq` `IsNoetherianRing.wfDvdMonoid` `Irreducible.associated_of_dvd` `Irreducible.not_isUnit` `Multiset.induction` `eq_or_ne` `pow_one` `Multiset.prod_cons` `Multiset.empty_eq_zero` `Multiset.prod_zero` `mul_one` `Multiset.mem_cons_self` `Multiset.mem_cons_of_mem` `pow_add` `mul_comm` `Associated.mul_mul` `eq_bot_iff` `Mathlib.Tactic.Push.not_and_eq` `IsLocalRing.le_maximalIdeal` `Ideal.unit_mul_mem_iff_mem` `Units.isUnit` `le_antisymm` `Mathlib.Tactic.Push.not_forall_eq` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `Ideal.pow_le_pow_right` `Nat.find_min'` `Ideal.pow_mem_pow` `dvd_refl` `IsScalarTower.left` `Ideal.span_singleton_pow` `Ideal.instIsTwoSided_1` `Ideal.span_le` `Set.singleton_subset_iff` `Nat.find_spec`
`maximalIdeal_isPrincipal_of_isDedekindDomain` 📖	mathematical	—	`Submodule.IsPrincipal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsLocalRing.maximalIdeal`	—	`bot_isPrincipal` `eq_bot_iff` `Mathlib.Tactic.Push.not_and_eq` `Ideal.span_le` `Set.singleton_subset_iff` `Ideal.radical_eq_sInf` `le_antisymm` `sInf_le` `Ideal.IsMaximal.isPrime'` `IsLocalRing.maximalIdeal.isMaximal` `le_sInf` `Eq.ge` `IsLocalRing.eq_maximalIdeal` `Ideal.IsPrime.isMaximal` `IsDedekindRing.toDimensionLEOne` `IsDedekindDomain.toIsDedekindRing` `Ideal.span_singleton_eq_bot` `Ideal.exists_radical_pow_le_of_fg` `IsNoetherian.noetherian` `IsDedekindRing.toIsNoetherian` `Nat.find_spec` `Ideal.IsMaximal.ne_top` `eq_top_iff` `LE.le.trans` `Ideal.one_eq_top` `pow_zero` `IsScalarTower.right` `Nat.find_eq_iff` `Ideal.mem_span_singleton'` `pow_succ` `Ideal.mul_mem_mul` `ZeroMemClass.zero_mem` `AddSubmonoidClass.toZeroMemClass` `Submodule.addSubmonoidClass` `IsLocalRing.toNontrivial` `IsDomain.to_noZeroDivisors` `RingHomSurjective.ids` `Iff.not` `IsFractionRing.to_map_eq_zero_iff` `Localization.isLocalization` `isIntegral_of_smul_mem_submodule` `instIsDomain` `IsLocalizedModule.instIsTorsionFreeLocalizationLocalizedModuleOfIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `NoZeroDivisors.toNoZeroSMulDivisors` `Submodule.ne_bot_iff` `Submodule.FG.map` `IsIntegrallyClosed.algebraMap_eq_of_integral` `IsDedekindRing.toIsIntegralClosure` `IsFractionRing.injective` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `div_mul_cancel₀` `IsScalarTower.to_smulCommClass'` `Mathlib.Tactic.Contrapose.contrapose₂` `mul_div_right_comm` `mul_div_cancel_right₀` `EuclideanDomain.toMulDivCancelClass` `IsLocalRing.le_maximalIdeal` `Submodule.mem_comap` `Ideal.eq_top_iff_one` `div_eq_one_iff_eq` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `mul_left_cancel₀` `IsCancelMulZero.toIsLeftCancelMulZero` `IsDomain.toIsCancelMulZero` `mul_assoc` `mul_comm` `Submodule.span_le`
`tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain` 📖	mathematical	—	`List.TFAE` `IsPrincipalIdealRing` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ValuationRing` `IsDedekindDomain` `IsIntegrallyClosed` `Submodule.IsPrincipal` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `IsLocalRing.maximalIdeal` `Module.finrank` `IsLocalRing.ResidueField` `IsLocalRing.CotangentSpace` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `IsLocalRing.ResidueField.field` `AddCommGroup.toAddCommMonoid` `Ideal.instAddCommGroupCotangent` `IsLocalRing.instModuleResidueFieldCotangentSpace`	—	`ValuationRing.instOfIsLocalRingOfIsBezout` `IsBezout.of_isPrincipalIdealRing` `List.TFAE.out` `IsBezout.TFAE` `ValuationRing.instIsBezout` `IsDedekindRing.toIsIntegralClosure` `IsDedekindDomain.toIsDedekindRing` `IsPrincipalIdealRing.isDedekindDomain` `IsLocalRing.eq_maximalIdeal` `Ideal.IsPrime.isMaximal` `IsDedekindRing.toDimensionLEOne` `IsLocalRing.maximalIdeal.isMaximal` `maximalIdeal_isPrincipal_of_isDedekindDomain` `IsLocalRing.finrank_cotangentSpace_le_one_iff` `IsScalarTower.right` `exists_maximalIdeal_pow_eq_of_principal` `ValuationRing.iff_ideal_total` `ne_of_not_le` `le_antisymm` `le_trans` `le_of_eq` `bot_le` `le_refl` `Mathlib.Tactic.Order.le_of_not_lt_le` `Mathlib.Tactic.Order.not_lt_of_not_le` `Ideal.pow_le_pow_right` `le_total` `List.tfae_of_cycle`

---

← Back to Index