CardinalEmb

📁 Source: Mathlib/FieldTheory/CardinalEmb.lean

Statistics

Metric	Count
Definitions embEquivPi, embFunctor, equivLim, equivSucc, factor, filtration, leastExt, succEquiv, wellOrderedBasis	9
Theorems adjoin_basis_eq_top, adjoin_image_leastExt, deg_lt_aleph0, directed_filtration, eq_bot_of_not_nonempty, equivLim_coherence, equivSucc_coherence, filtration_apply, filtration_succ, iSup_adjoin_eq_top, iSup_filtration, instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, isLeast_leastExt, noMaxOrder_rank_toType, strictMono_filtration, strictMono_leastExt, succEquiv_coherence, two_le_deg, cardinal_eq, cardinal_eq_of_isSeparable, cardinal_eq_two_pow_rank, cardinal_eq_two_pow_sepDegree	24
Total	33

Field.Emb

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinal_eq 📖	mathematical	—	Field.Emb Field.sepDegree	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.left cardinal_separableClosure cardinal_eq_of_isSeparable separableClosure.isSeparable
cardinal_eq_of_isSeparable 📖	mathematical	—	Field.Emb Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring	—	Nat.instAtLeastTwoHAddOfNat cardinal_eq_two_pow_rank Module.finrank_eq_rank commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite IsNoetherian.iff_rank_lt_aleph0 not_le Module.Projective.of_free Module.Free.of_divisionRing Cardinal.toNat_eq_iff LT.lt.ne' Module.finrank_pos instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Nat.card.eq_1 Field.finSepDegree.eq_1 Field.finSepDegree_eq_finrank_of_isSeparable
cardinal_eq_two_pow_rank 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0 Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring	Field.Emb Cardinal.instPowCardinal instOfNatAtLeastTwo Cardinal.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Algebra.IsSeparable.isAlgebraic IsLocalRing.toNontrivial Field.instIsLocalRing Equiv.cardinal_eq Cardinal.mk_pi le_antisymm Cardinal.power_eq_two_power Cardinal.natCast_le_aleph0 Cardinal.mk_ord_toType Cardinal.prod_const' Cardinal.prod_le_prod LT.lt.le Cardinal.deg_lt_aleph0 Cardinal.two_le_deg
cardinal_eq_two_pow_sepDegree 📖	mathematical	Cardinal Cardinal.instLE Cardinal.aleph0 Field.sepDegree	Field.Emb Cardinal.instPowCardinal instOfNatAtLeastTwo Cardinal.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat IsScalarTower.left cardinal_separableClosure cardinal_eq_two_pow_rank separableClosure.isSeparable

Field.Emb.Cardinal

Definitions

Name	Category	Theorems
embEquivPi 📖	CompOp	—
embFunctor 📖	CompOp	3 math math: equivLim_coherence, instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, equivSucc_coherence
equivLim 📖	CompOp	1 math math: equivLim_coherence
equivSucc 📖	CompOp	1 math math: equivSucc_coherence
factor 📖	CompOp	1 math math: equivSucc_coherence
filtration 📖	CompOp	7 math math: equivLim_coherence, directed_filtration, instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor, equivSucc_coherence, eq_bot_of_not_nonempty, filtration_apply, iSup_filtration
leastExt 📖	CompOp	12 math math: filtration_succ, two_le_deg, isLeast_leastExt, succEquiv_coherence, instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, strictMono_leastExt, filtration_apply, deg_lt_aleph0, strictMono_filtration, iSup_adjoin_eq_top, adjoin_image_leastExt, instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet
succEquiv 📖	CompOp	1 math math: succEquiv_coherence
wellOrderedBasis 📖	CompOp	12 math math: filtration_succ, two_le_deg, isLeast_leastExt, succEquiv_coherence, instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, filtration_apply, deg_lt_aleph0, strictMono_filtration, iSup_adjoin_eq_top, adjoin_image_leastExt, instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet, adjoin_basis_eq_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_basis_eq_top 📖	mathematical	—	IntermediateField.adjoin Set.range Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring DFunLike.coe Module.Basis Module.Basis.instFunLike wellOrderedBasis Top.top IntermediateField OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	IntermediateField.toSubalgebra_injective Subalgebra.toSubmodule_injective top_unique LE.le.trans Eq.ge Module.Basis.span_eq Algebra.span_le_adjoin IntermediateField.algebra_adjoin_le_adjoin
adjoin_image_leastExt 📖	mathematical	—	IntermediateField.adjoin Set.image Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring DFunLike.coe Module.Basis Module.Basis.instFunLike wellOrderedBasis leastExt Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType	—	le_antisymm IntermediateField.adjoin.mono Set.image_comp Set.image_mono strictMono_leastExt IntermediateField.adjoin_le_iff Mathlib.Tactic.Contrapose.contrapose₁ LE.le.not_gt isLeast_leastExt
deg_lt_aleph0 📖	mathematical	—	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Field.Emb IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set.image Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring DFunLike.coe Module.Basis Module.Basis.instFunLike wellOrderedBasis leastExt Set.Iio SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType IntermediateField.toField IntermediateField.instAlgebraSubtypeMem Algebra.id Set Set.instSingletonSet IntermediateField.instAlgebraSubtypeMem_1 Cardinal.aleph0	—	Cardinal.lt_aleph0_of_finite Finite.algHom Module.Free.of_divisionRing instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet instIsDomain
directed_filtration 📖	mathematical	—	Directed IntermediateField Set.Elem WithTop Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring Set.Iio WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType Preorder.toLE IntermediateField.instPartialOrder DFunLike.coe OrderEmbedding instFunLikeOrderEmbedding filtration Set Set.instMembership	—	Monotone.directed_le SemilatticeSup.instIsDirectedOrder Monotone.comp OrderEmbedding.monotone Subtype.mono_coe
eq_bot_of_not_nonempty 📖	mathematical	Order.IsSuccPrelimit WithTop Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType Set.Elem Set.Iio	DFunLike.coe OrderEmbedding IntermediateField Preorder.toLE IntermediateField.instPartialOrder instFunLikeOrderEmbedding filtration Bot.bot OrderBot.toBot SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Cardinal.mk_ne_zero_iff LT.lt.ne' LT.lt.trans_eq rank_pos instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors IsLocalRing.toNontrivial Field.instIsLocalRing Cardinal.mk_ord_toType WithTop.range_coe Set.instNonemptyRange bot_unique IntermediateField.adjoin_le_iff WithTop.coe_lt_coe
equivLim_coherence 📖	mathematical	Order.IsSuccPrelimit WithTop Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType	Set Set.instMembership InverseSystem.limit AlgHom IntermediateField SetLike.instMembership IntermediateField.instSetLike DFunLike.coe OrderEmbedding Preorder.toLE IntermediateField.instPartialOrder instFunLikeOrderEmbedding filtration AlgebraicClosure IntermediateField.toField AlgebraicClosure.instField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AlgebraicClosure.instAlgebra embFunctor Equiv Set.Elem EquivLike.toFunLike Equiv.instEquivLike equivLim Set.Iio LT.lt.le Set.mem_Iio	—	IsScalarTower.left
equivSucc_coherence 📖	mathematical	—	AlgHom IntermediateField SetLike.instMembership IntermediateField.instSetLike DFunLike.coe OrderEmbedding WithTop Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType IntermediateField.instPartialOrder instFunLikeOrderEmbedding filtration AlgebraicClosure IntermediateField.toField AlgebraicClosure.instField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AlgebraicClosure.instAlgebra factor Equiv Order.succ WithTop.instSuccOrder EquivLike.toFunLike Equiv.instEquivLike equivSucc embFunctor Order.le_succ	—	IsScalarTower.left Order.le_succ succEquiv_coherence
filtration_apply 📖	mathematical	—	DFunLike.coe RelEmbedding WithTop Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring IntermediateField Preorder.toLE WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType IntermediateField.instPartialOrder RelEmbedding.instFunLike filtration WithTop.recTopCoe Top.top OrderTop.toTop SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice IntermediateField.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder IntermediateField.adjoin Set.image Module.Basis Module.Basis.instFunLike wellOrderedBasis leastExt Set.Iio	—	Set.image_congr
filtration_succ 📖	mathematical	—	IntermediateField.adjoin Set.image Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring DFunLike.coe Module.Basis Module.Basis.instFunLike wellOrderedBasis leastExt Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType Order.succ IntermediateField.restrictScalars IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.toField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction IntermediateField.instAlgebraSubtypeMem IntermediateField.isScalarTower_mid' Set Set.instSingletonSet	—	IsScalarTower.left IntermediateField.isScalarTower_mid' Order.Iio_succ noMaxOrder_rank_toType Set.Iio_insert Set.image_insert_eq Set.union_singleton IntermediateField.adjoin_adjoin_left
iSup_adjoin_eq_top 📖	mathematical	—	iSup IntermediateField Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice IntermediateField.instCompleteLattice IntermediateField.adjoin Set.image DFunLike.coe Module.Basis Module.Basis.instFunLike wellOrderedBasis leastExt Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	adjoin_image_leastExt le_iSup IntermediateField.subset_adjoin LT.lt.trans_le Order.lt_succ noMaxOrder_rank_toType StrictMono.le_apply wellFoundedLT_toType strictMono_leastExt
iSup_filtration 📖	mathematical	Order.IsSuccPrelimit WithTop Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring Preorder.toLT WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType	iSup IntermediateField Set.Elem Set.Iio ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice IntermediateField.instCompleteLattice DFunLike.coe OrderEmbedding Preorder.toLE IntermediateField.instPartialOrder instFunLikeOrderEmbedding filtration Set Set.instMembership	—	WithTop.range_coe iSup_range' iSup_adjoin_eq_top LE.le.antisymm iSup_le OrderEmbedding.monotone LT.lt.le Set.mem_Iio IntermediateField.adjoin_le_iff le_iSup Order.IsSuccPrelimit.succ_lt WithTop.coe_lt_coe IntermediateField.subset_adjoin Order.lt_succ noMaxOrder_rank_toType
instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet 📖	mathematical	—	FiniteDimensional IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set.image Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring DFunLike.coe Module.Basis Module.Basis.instFunLike wellOrderedBasis leastExt Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType IntermediateField.toField IntermediateField.instAlgebraSubtypeMem Algebra.id Set Set.instSingletonSet Field.toDivisionRing Ring.toAddCommGroup DivisionRing.toRing IntermediateField.instModuleSubtypeMem_1	—	IntermediateField.adjoin.finiteDimensional IsAlgebraic.isIntegral Algebra.IsAlgebraic.isAlgebraic Algebra.IsAlgebraic.tower_top IsScalarTower.left IntermediateField.isScalarTower_mid'
instInverseSystemWithTopToTypeOrdRankAlgHomSubtypeMemIntermediateFieldCoeOrderEmbeddingFiltrationAlgebraicClosureEmbFunctor 📖	mathematical	—	InverseSystem WithTop Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring WithTop.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType AlgHom IntermediateField SetLike.instMembership IntermediateField.instSetLike DFunLike.coe OrderEmbedding Preorder.toLE IntermediateField.instPartialOrder instFunLikeOrderEmbedding filtration AlgebraicClosure IntermediateField.toField AlgebraicClosure.instField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AlgebraicClosure.instAlgebra embFunctor	—	IsScalarTower.left le_rfl
instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet 📖	mathematical	—	Algebra.IsSeparable IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set.image Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring DFunLike.coe Module.Basis Module.Basis.instFunLike wellOrderedBasis leastExt Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType IntermediateField.toField IntermediateField.instAlgebraSubtypeMem Algebra.id Set Set.instSingletonSet DivisionRing.toRing Field.toDivisionRing IntermediateField.instAlgebraSubtypeMem_1	—	Algebra.isSeparable_tower_top_of_isSeparable IsScalarTower.left IntermediateField.isScalarTower_mid' IsScalarTower.of_algebraMap_eq' SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass Algebra.isSeparable_tower_bot_of_isSeparable IsLocalRing.toNontrivial Field.instIsLocalRing
isLeast_leastExt 📖	mathematical	—	IsLeast Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType setOf IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set.image DFunLike.coe Module.Basis Module.Basis.instFunLike wellOrderedBasis leastExt Set.Iio	—	Set.image_eq_range leastExt.eq_1 wellFounded_lt wellFoundedLT_toType WellFounded.min_mem WellFounded.min_le
noMaxOrder_rank_toType 📖	mathematical	—	NoMaxOrder Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType	—	Cardinal.noMaxOrder Fact.out
strictMono_filtration 📖	mathematical	—	StrictMono Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring IntermediateField PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType IntermediateField.instPartialOrder IntermediateField.adjoin Set.image DFunLike.coe Module.Basis Module.Basis.instFunLike wellOrderedBasis leastExt Set.Iio	—	IntermediateField.adjoin.mono Set.image_mono Set.Iio_subset_Iio LT.lt.le isLeast_leastExt IntermediateField.subset_adjoin
strictMono_leastExt 📖	mathematical	—	StrictMono Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType leastExt	—	isLeast_leastExt LE.le.eq_or_lt IntermediateField.subset_adjoin LE.le.not_gt IntermediateField.adjoin.mono Set.image_mono LT.lt.trans
succEquiv_coherence 📖	mathematical	—	AlgHom IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set.image Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring DFunLike.coe Module.Basis Module.Basis.instFunLike wellOrderedBasis leastExt Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType AlgebraicClosure IntermediateField.toField AlgebraicClosure.instField IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction AlgebraicClosure.instAlgebra Field.Emb IntermediateField.instAlgebraSubtypeMem Set Set.instSingletonSet IntermediateField.instAlgebraSubtypeMem_1 Equiv Order.succ EquivLike.toFunLike Equiv.instEquivLike succEquiv AlgHom.comp Subalgebra Subalgebra.instSetLike IntermediateField.toSubalgebra Subalgebra.toSemiring Subalgebra.algebra Subalgebra.inclusion StrictMono.monotone IntermediateField.instPartialOrder strictMono_filtration Order.le_succ	—	IsScalarTower.left AlgHom.ext StrictMono.monotone strictMono_filtration Order.le_succ filtration_succ
two_le_deg 📖	mathematical	—	Cardinal Cardinal.instLE instOfNatAtLeastTwo Cardinal.instNatCast Nat.instAtLeastTwoHAddOfNat Field.Emb IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set.image Ordinal.ToType Cardinal.ord Module.rank DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Semifield.toCommSemiring DFunLike.coe Module.Basis Module.Basis.instFunLike wellOrderedBasis leastExt Set.Iio PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder_toType IntermediateField.toField IntermediateField.instAlgebraSubtypeMem Algebra.id Set Set.instSingletonSet IntermediateField.instAlgebraSubtypeMem_1	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_ofNat Cardinal.toNat_le_iff_le_of_lt_aleph0 Cardinal.natCast_lt_aleph0 deg_lt_aleph0 Cardinal.toNat_natCast Nat.card.eq_1 Field.finSepDegree.eq_1 Field.finSepDegree_eq_finrank_of_isSeparable instIsSeparableSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet IsScalarTower.left IntermediateField.finrank_adjoin_simple_eq_one_iff LE.le.antisymm Module.finrank_pos commRing_strongRankCondition SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass IntermediateField.instSubfieldClass IsLocalRing.toNontrivial Field.instIsLocalRing instFiniteDimensionalSubtypeMemIntermediateFieldAdjoinImageToTypeOrdRankCompCoeBasisWellOrderedBasisLeastExtIioSingletonSet instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors isLeast_leastExt

---

← Back to Index