FunctionField

📁 Source: Mathlib/NumberTheory/FunctionField.lean

Statistics

Metric	Count
Definitions FunctionField, FqtInfty, inftyValuation, inftyValuationDef, inftyValuedFqt, instFieldFqtInfty, instInhabitedFqtInfty, ringOfIntegers, valuedFqtInfty, FunctionField	10
Theorems map_add_le_max', map_mul', map_one', map_zero', algebraMap_injective, C, X, X_inv, X_zpow, polynomial, inftyValuation_apply, inftyValuation_of_nonzero, def, instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation, algebraMap_injective, instIsDedekindDomainSubtypeMemSubalgebraPolynomialOfIsSeparableRatFunc, instIsDomainSubtypeMemSubalgebraPolynomial, instIsFractionRingSubtypeMemSubalgebraPolynomial, instIsIntegralClosureSubtypeMemSubalgebraPolynomial, instIsIntegrallyClosedSubtypeMemSubalgebraPolynomial, instIsNoetherianPolynomialSubtypeMemSubalgebraOfIsSeparableRatFunc, not_isField, def, functionField_iff	24
Total	34

FunctionField

Definitions

Name	Category	Theorems
FqtInfty 📖	CompOp	1 math math: valuedFqtInfty.def
inftyValuation 📖	CompOp	6 math math: inftyValuation.X_inv, instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation, inftyValuation.X_zpow, inftyValuation.X, inftyValuation.C, inftyValuation_apply
inftyValuationDef 📖	CompOp	8 math math: InftyValuation.map_zero', inftyValuation.polynomial, inftyValuation_of_nonzero, InftyValuation.map_add_le_max', InftyValuation.map_one', InftyValuation.map_mul', inftyValuedFqt.def, inftyValuation_apply
inftyValuedFqt 📖	CompOp	2 math math: valuedFqtInfty.def, inftyValuedFqt.def
instFieldFqtInfty 📖	CompOp	1 math math: valuedFqtInfty.def
instInhabitedFqtInfty 📖	CompOp	—
ringOfIntegers 📖	CompOp	9 math math: ringOfIntegers.instIsIntegralClosureSubtypeMemSubalgebraPolynomial, classNumber_eq_one_iff, ringOfIntegers.instIsDomainSubtypeMemSubalgebraPolynomial, ringOfIntegers.instIsIntegrallyClosedSubtypeMemSubalgebraPolynomial, ringOfIntegers.instIsDedekindDomainSubtypeMemSubalgebraPolynomialOfIsSeparableRatFunc, ringOfIntegers.algebraMap_injective, ringOfIntegers.instIsFractionRingSubtypeMemSubalgebraPolynomial, ringOfIntegers.instIsNoetherianPolynomialSubtypeMemSubalgebraOfIsSeparableRatFunc, ringOfIntegers.not_isField
valuedFqtInfty 📖	CompOp	1 math math: valuedFqtInfty.def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_injective 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.commSemiring Semifield.toCommSemiring RingHom.instFunLike algebraMap	—	instIsDomain IsScalarTower.right IsScalarTower.algebraMap_eq RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing IsFractionRing.injective RatFunc.instIsFractionRingPolynomial
inftyValuation_apply 📖	mathematical	—	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike inftyValuation inftyValuationDef	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing instIsDomain
inftyValuation_of_nonzero 📖	mathematical	—	inftyValuationDef WithZero.exp RatFunc.intDegree	—	inftyValuationDef.eq_1
instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation 📖	mathematical	—	Valuation.IsNontrivial RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing inftyValuation	—	instIsDomain Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing inftyValuation.X

FunctionField.InftyValuation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_add_le_max' 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt FunctionField.inftyValuationDef RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain RatFunc.instAdd SemilatticeSup.toMax WithZero.semilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeOfLinearOrder Multiplicative.linearOrder Int.instLinearOrder	—	instIsDomain zero_add FunctionField.inftyValuationDef.eq_1 max_eq_right WithZero.zero_le le_refl add_zero max_comm zero_le' Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing RatFunc.intDegree_add_le
map_mul' 📖	mathematical	—	FunctionField.inftyValuationDef RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain RatFunc.instMul WithZero Multiplicative MulZeroClass.toMul WithZero.instMulZeroClass Multiplicative.mul	—	FunctionField.inftyValuationDef.eq_1 MulZeroClass.zero_mul MulZeroClass.mul_zero IsDomain.to_noZeroDivisors instIsDomain RatFunc.intDegree_mul
map_one' 📖	mathematical	—	FunctionField.inftyValuationDef RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain RatFunc.instOne WithZero Multiplicative WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	one_ne_zero NeZero.one instIsDomain RatFunc.instNontrivial IsLocalRing.toNontrivial Field.instIsLocalRing RatFunc.intDegree_one
map_zero' 📖	mathematical	—	FunctionField.inftyValuationDef RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain RatFunc.instZero WithZero Multiplicative WithZero.instZero	—	—

FunctionField.inftyValuation

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C 📖	mathematical	—	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike FunctionField.inftyValuation RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike RatFunc.C WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing instIsDomain FunctionField.inftyValuation_of_nonzero RatFunc.instNontrivial IsLocalRing.toNontrivial Field.instIsLocalRing RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RatFunc.intDegree_C
X 📖	mathematical	—	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike FunctionField.inftyValuation RatFunc.X WithZero.exp	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing instIsDomain RatFunc.intDegree_X RatFunc.X_ne_zero
X_inv 📖	mathematical	—	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike FunctionField.inftyValuation RatFunc.instDiv RatFunc.instOne RatFunc.X WithZero.exp	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing instIsDomain one_div zpow_neg_one X_zpow
X_zpow 📖	mathematical	—	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike FunctionField.inftyValuation DivInvMonoid.toZPow DivisionRing.toDivInvMonoid RatFunc.X WithZero.exp	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing instIsDomain map_zpow₀ ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass X mul_one
polynomial 📖	mathematical	—	FunctionField.inftyValuationDef DFunLike.coe RingHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.commSemiring Semifield.toCommSemiring RatFunc.instField instIsDomain RingHom.instFunLike algebraMap RatFunc.instAlgebraOfPolynomial Algebra.id WithZero.exp Polynomial.natDegree	—	instIsDomain FunctionField.inftyValuationDef.eq_1 Module.IsTorsionFree.to_faithfulSMul Polynomial.instIsCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsDomain.toIsCancelMulZero RatFunc.instNontrivial IsLocalRing.toNontrivial Field.instIsLocalRing FaithfulSMul.to_isTorsionFree IsFractionRing.instFaithfulSMul RatFunc.instIsFractionRingPolynomial Polynomial.nontrivial RatFunc.intDegree_polynomial

FunctionField.inftyValuedFqt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
def 📖	mathematical	—	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike Valued.v FunctionField.inftyValuedFqt FunctionField.inftyValuationDef	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid instIsDomain

FunctionField.ringOfIntegers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_injective 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subalgebra CommRing.toCommSemiring Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike FunctionField.ringOfIntegers DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.commSemiring Semifield.toCommSemiring Subalgebra.toSemiring RingHom.instFunLike algebraMap Subalgebra.algebra	—	instIsDomain IsScalarTower.right IsScalarTower.algebraMap_eq RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing IsFractionRing.injective RatFunc.instIsFractionRingPolynomial injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass Subalgebra.instSubsemiringClass Subalgebra.coe_zero
instIsDedekindDomainSubtypeMemSubalgebraPolynomialOfIsSeparableRatFunc 📖	mathematical	—	IsDedekindDomain Subalgebra Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommRing.toCommSemiring Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike FunctionField.ringOfIntegers Subalgebra.toCommRing	—	instIsDomain IsScalarTower.right IsIntegralClosure.isDedekindDomain RatFunc.instIsFractionRingPolynomial instIsIntegralClosureSubtypeMemSubalgebraPolynomial IsScalarTower.subalgebra' Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd instIsDomainSubtypeMemSubalgebraPolynomial IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain
instIsDomainSubtypeMemSubalgebraPolynomial 📖	mathematical	—	IsDomain Subalgebra Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommRing.toCommSemiring Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike FunctionField.ringOfIntegers Subalgebra.toSemiring	—	Subalgebra.isDomain instIsDomain
instIsFractionRingSubtypeMemSubalgebraPolynomial 📖	mathematical	—	IsFractionRing Subalgebra Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommRing.toCommSemiring Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike FunctionField.ringOfIntegers Subalgebra.toCommSemiring Semifield.toCommSemiring Subalgebra.toAlgebra Algebra.id	—	instIsDomain IsScalarTower.right integralClosure.isFractionRing_of_finite_extension RatFunc.instIsFractionRingPolynomial Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd
instIsIntegralClosureSubtypeMemSubalgebraPolynomial 📖	mathematical	—	IsIntegralClosure Subalgebra Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommRing.toCommSemiring Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike FunctionField.ringOfIntegers Subalgebra.toCommSemiring Semifield.toCommSemiring Subalgebra.toAlgebra Algebra.id	—	integralClosure.isIntegralClosure
instIsIntegrallyClosedSubtypeMemSubalgebraPolynomial 📖	mathematical	—	IsIntegrallyClosed Subalgebra Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommRing.toCommSemiring Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike FunctionField.ringOfIntegers Subalgebra.toCommRing	—	instIsDomain IsScalarTower.right integralClosure.isIntegrallyClosedOfFiniteExtension RatFunc.instIsFractionRingPolynomial Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd
instIsNoetherianPolynomialSubtypeMemSubalgebraOfIsSeparableRatFunc 📖	mathematical	—	IsNoetherian Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subalgebra CommRing.toCommSemiring Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike FunctionField.ringOfIntegers Polynomial.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Subalgebra.toCommRing Subalgebra.instModuleSubtypeMem	—	instIsDomain IsScalarTower.right IsIntegralClosure.isNoetherian RatFunc.instIsFractionRingPolynomial instIsIntegralClosureSubtypeMemSubalgebraPolynomial IsScalarTower.subalgebra' Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsDedekindRing.toIsIntegralClosure IsDedekindDomain.toIsDedekindRing IsPrincipalIdealRing.isDedekindDomain EuclideanDomain.to_principal_ideal_domain Polynomial.isNoetherianRing IsDedekindRing.toIsNoetherian
not_isField 📖	mathematical	—	IsField Subalgebra Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield CommRing.toCommSemiring Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike FunctionField.ringOfIntegers Subalgebra.toSemiring	—	instIsDomain IsScalarTower.right Algebra.IsIntegral.isField_iff_isField IsIntegralClosure.isIntegral_algebra instIsIntegralClosureSubtypeMemSubalgebraPolynomial IsScalarTower.subalgebra' instIsDomainSubtypeMemSubalgebraPolynomial algebraMap_injective Polynomial.not_isField

FunctionField.valuedFqtInfty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
def 📖	mathematical	—	DFunLike.coe Valuation FunctionField.FqtInfty WithZero Multiplicative LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing FunctionField.instFieldFqtInfty Valuation.instFunLike Valued.v FunctionField.valuedFqtInfty Valued.extension RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain RatFunc.instField instIsDomain Field.toSemifield FunctionField.inftyValuedFqt	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid

WeierstrassCurve.Affine

Definitions

Name	Category	Theorems
FunctionField 📖	CompOp	5 math math: CoordinateRing.mk_XYIdeal'_neg_mul, CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', Point.toClass_some, CoordinateRing.XYIdeal'_eq, Point.toClass_apply

(root)

Definitions

Name	Category	Theorems
FunctionField 📖	MathDef	1 math math: functionField_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functionField_iff 📖	mathematical	—	FunctionField FiniteDimensional Field.toDivisionRing Ring.toAddCommGroup DivisionRing.toRing Algebra.toModule Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	instIsDomain IsScalarTower.right RatFunc.instIsFractionRingPolynomial Algebra.smul_def IsLocalization.ext map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass RingHom.instRingHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass AlgEquiv.commutes commRing_strongRankCondition RatFunc.instNontrivial IsLocalRing.toNontrivial Field.instIsLocalRing Module.free_of_finite_type_torsion_free' EuclideanDomain.to_principal_ideal_domain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Module.Basis.finiteDimensional_of_finite Finite.of_fintype AlgEquivClass.toRingEquivClass AlgEquiv.apply_symm_apply

---

← Back to Index