tfae

📁 Source: MathlibTest/tfae.lean

Statistics

Metric	Count
Definitions	0
Theorems tfae, tfae, tfae, tfae	4
Total	4

IsArtinianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tfae 📖	mathematical	—	List.TFAE Module.Finite Ring.toSemiring AddCommGroup.toAddCommMonoid IsNoetherian IsArtinian IsFiniteLength	—	IsSemiprimaryRing.isNoetherian_iff_isArtinian instIsSemiprimaryRing Module.IsNoetherian.finite isArtinian_of_fg_of_artinian' isFiniteLength_iff_isNoetherian_isArtinian List.tfae_of_cycle

IsGalois

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tfae 📖	mathematical	—	List.TFAE IsGalois IntermediateField IntermediateField.fixedField Top.top Subgroup AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring AlgEquiv.aut Subgroup.instTop Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder Nat.card Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Polynomial Polynomial.Separable Polynomial.IsSplittingField	—	OrderIso.map_bot card_aut_eq_finrank is_separable_splitting_field of_fixedField_eq_bot of_card_aut_eq_finrank of_separable_splitting_field List.tfae_of_cycle

IsLocallyConstant

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tfae 📖	mathematical	—	List.TFAE IsLocallyConstant	—	IsOpen.mem_nhds mem_nhds_iff isOpen_iff_forall_mem_open Set.mem_preimage List.tfae_of_cycle

IsSimpleRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
tfae 📖	mathematical	—	List.TFAE IsSemisimpleRing IsArtinianRing Ring.toSemiring Ideal IsAtom PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instOrderBot	—	instIsArtinianOfIsSemisimpleModuleOfFinite Module.Finite.self IsAtomic.exists_atom Ideal.instNontrivial instNontrivial IsStronglyAtomic.isAtomic instIsStronglyAtomicOfWellFoundedLT isSimpleRing_iff_isTwoSided_imp isSimpleModule_iff_isAtom Submodule.IsFullyInvariant.isotypicComponent LT.lt.not_ge IsAtom.bot_lt LE.le.trans_eq le_sSup IsSemisimpleModule.congr instIsSemisimpleModuleSubtypeMemSubmoduleIsotypicComponent instIsSemisimpleModuleOfIsSimpleModule RingHomInvPair.ids RingHomCompTriple.ids List.tfae_of_cycle

---

← Back to Index