Field

📁 Source: Mathlib/RingTheory/Smooth/Field.lean

Statistics

Metric	Count
Definitions	0
Theorems adjoin_of_algebraicIndependent, of_algebraicIndependent, of_algebraicIndependent_of_isSeparable, of_perfectField	4
Total	4

Algebra.FormallySmooth

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_of_algebraicIndependent 📖	mathematical	AlgebraicIndependent EuclideanDomain.toCommRing Field.toEuclideanDomain	Algebra.FormallySmooth IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set.range IntermediateField.toField IntermediateField.algebra' CommRing.toCommSemiring Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule	—	of_equiv Algebra.mvPolynomial of_isLocalization IntermediateField.algebraAdjoinAdjoin.instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin comp IsScalarTower.left IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin
of_algebraicIndependent 📖	mathematical	AlgebraicIndependent EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField.adjoin Set.range Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	Algebra.FormallySmooth	—	IsScalarTower.left adjoin_of_algebraicIndependent of_equiv
of_algebraicIndependent_of_isSeparable 📖	mathematical	AlgebraicIndependent EuclideanDomain.toCommRing Field.toEuclideanDomain	Algebra.FormallySmooth	—	IsScalarTower.left adjoin_of_algebraicIndependent Algebra.EssFiniteType.of_comp IntermediateField.isScalarTower_mid' Algebra.FormallyEtale.iff_isSeparable comp Algebra.FormallyEtale.instFormallySmooth
of_perfectField 📖	mathematical	—	Algebra.FormallySmooth EuclideanDomain.toCommRing Field.toEuclideanDomain	—	exists_isTranscendenceBasis_and_isSeparable_of_perfectField Subtype.range_coe_subtype SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass of_algebraicIndependent_of_isSeparable

---

← Back to Index