TFAE

📁 Source: Mathlib/Tactic/TFAE.lean

Statistics

Metric	Count
Definitions binder, impArrow, impFrom, impIff, impTo, tfaeHaveDecl, tfaeHaveEqnsDecl, tfaeHaveIdDecl, tfaeHaveIdLhs, tfaeHavePatDecl, tfaeType, dfs, elabIndex, elabTFAEType, getTFAEList, mkTFAEId, proveChain, proveGetLastDImpl, proveImpl, proveTFAE, tfaeFinish, tfaeHave, tfaeHave', useDeprecated	24
Theorems TFAE, TFAE, TFAE, TFAE, TFAE	5
Total	29

ContinuousLinearMap.IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
TFAE 📖	mathematical	IsIdempotentElem ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace ContinuousLinearMap.instMul	List.TFAE Submodule DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace Submodule.orthogonal LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids ContinuousLinearMap.toLinearMap LinearMap.ker IsStarNormal ContinuousLinearMap ContinuousLinearMap.instMul ContinuousLinearMap.instStarId IsSelfAdjoint ContinuousLinearMap.IsPositive	—	isSelfAdjoint_iff_isStarNormal isPositive_iff_isSelfAdjoint RingHomSurjective.ids LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range toLinearMap ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric List.tfae_of_cycle

HenselianLocalRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
TFAE 📖	mathematical	—	List.TFAE HenselianLocalRing	—	Ideal.Quotient.mk_surjective mem_nonunits_iff Polynomial.eval₂_at_apply Ideal.instIsTwoSided_1 Ideal.Quotient.eq_zero_iff_mem map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass sub_eq_zero toIsLocalRing is_henselian IsLocalRing.ker_eq_maximalIdeal Mathlib.Tactic.Contrapose.contrapose₂ RingHom.mem_ker IsLocalRing.mem_maximalIdeal RingHom.map_sub List.tfae_of_cycle

IsBezout

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
TFAE 📖	mathematical	—	List.TFAE IsNoetherianRing CommSemiring.toSemiring CommRing.toCommSemiring IsPrincipalIdealRing UniqueFactorizationMonoid CommSemiring.toCommMonoidWithZero WfDvdMonoid	—	IsPrincipalIdealRing.of_isNoetherianRing_of_isBezout PrincipalIdealRing.to_uniqueFactorizationMonoid UniqueFactorizationMonoid.toIsWellFounded isNoetherianRing_iff isNoetherian_iff_fg_wellFounded RelEmbedding.wellFounded Submodule.IsPrincipal.principal isPrincipal_of_FG Ideal.span_singleton_lt_span_singleton List.tfae_of_cycle

IsDiscreteValuationRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
TFAE 📖	mathematical	IsField CommSemiring.toSemiring CommRing.toCommSemiring	List.TFAE IsDiscreteValuationRing ValuationRing IsDedekindDomain IsIntegrallyClosed ExistsUnique Ideal CommSemiring.toSemiring CommRing.toCommSemiring Bot.bot Submodule.instBot NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.IsPrime Submodule.IsPrincipal IsLocalRing.maximalIdeal Module.finrank IsLocalRing.ResidueField IsLocalRing.CotangentSpace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field AddCommGroup.toAddCommMonoid Ideal.instAddCommGroupCotangent IsLocalRing.instModuleResidueFieldCotangentSpace	—	IsScalarTower.right Iff.not IsLocalRing.isField_iff_maximalIdeal_eq toIsPrincipalIdealRing ExistsUnique.unique Ideal.IsMaximal.isPrime' IsLocalRing.maximalIdeal.isMaximal tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain

Mathlib.Tactic.TFAE

Definitions

Name	Category	Theorems
dfs 📖	CompOp	—
elabIndex 📖	CompOp	—
elabTFAEType 📖	CompOp	—
getTFAEList 📖	CompOp	—
mkTFAEId 📖	CompOp	—
proveChain 📖	CompOp	—
proveGetLastDImpl 📖	CompOp	—
proveImpl 📖	CompOp	—
proveTFAE 📖	CompOp	—
tfaeFinish 📖	CompOp	—
tfaeHave 📖	CompOp	—
tfaeHave' 📖	CompOp	—
useDeprecated 📖	CompOp	—

Mathlib.Tactic.TFAE.Parser

Definitions

Name	Category	Theorems
binder 📖	CompOp	—
impArrow 📖	CompOp	—
impFrom 📖	CompOp	—
impIff 📖	CompOp	—
impTo 📖	CompOp	—
tfaeHaveDecl 📖	CompOp	—
tfaeHaveEqnsDecl 📖	CompOp	—
tfaeHaveIdDecl 📖	CompOp	—
tfaeHaveIdLhs 📖	CompOp	—
tfaeHavePatDecl 📖	CompOp	—
tfaeType 📖	CompOp	—

ValuationRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
TFAE 📖	mathematical	—	List.TFAE ValuationRing semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsLocalRing IsBezout	—	IsDomain.toNontrivial IsDomain.to_noZeroDivisors iff_isInteger_or_isInteger Localization.isLocalization iff_dvd_total iff_ideal_total iff_local_bezout_domain List.tfae_of_cycle

---

← Back to Index