AlgebraInstances

📁 Source: Mathlib/RingTheory/Valuation/AlgebraInstances.lean

Statistics

Metric	Count
Definitions algebra, equiv, instAlgebraSubtypeMemValuationSubringWithZeroMultiplicativeInt	3
Theorems algebraMap_injective, instIsScalarTowerSubtypeMemValuationSubringWithZeroMultiplicativeInt, integralClosure_algebraMap_injective, isIntegral_of_mem_ringOfIntegers, isIntegral_of_mem_ringOfIntegers'	5
Total	8

ValuationSubring

Definitions

Name	Category	Theorems
algebra 📖	CompOp	—
equiv 📖	CompOp	—
instAlgebraSubtypeMemValuationSubringWithZeroMultiplicativeInt 📖	CompOp	4 math math: integralClosure_algebraMap_injective, instIsScalarTowerSubtypeMemValuationSubringWithZeroMultiplicativeInt, isIntegral_of_mem_ringOfIntegers', algebraMap_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_injective 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike Valuation.valuationSubring WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap instAlgebraSubtypeMemValuationSubringWithZeroMultiplicativeInt	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing IsFractionRing.injective instIsFractionRingSubtypeMem
instIsScalarTowerSubtypeMemValuationSubringWithZeroMultiplicativeInt 📖	mathematical	—	IsScalarTower ValuationSubring SetLike.instMembership instSetLike Valuation.valuationSubring WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid Algebra.toSMul SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring instAlgebraSubtypeMemValuationSubringWithZeroMultiplicativeInt	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid SubringClass.toSubsemiringClass instSubringClass Submonoid.instIsScalarTowerSubtypeMem
integralClosure_algebraMap_injective 📖	mathematical	—	ValuationSubring SetLike.instMembership instSetLike Valuation.valuationSubring WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid Subalgebra CommRing.toCommSemiring instCommRingSubtypeMem CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instAlgebraSubtypeMemValuationSubringWithZeroMultiplicativeInt Subalgebra.instSetLike integralClosure DFunLike.coe RingHom Semiring.toNonAssocSemiring SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing Field.toDivisionRing instSubringClass Subalgebra.toSemiring RingHom.instFunLike algebraMap Subalgebra.algebra	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing FaithfulSMul.algebraMap_injective Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid SubringClass.toSubsemiringClass instSubringClass Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero instIsDomainSubtypeMem SubsemiringClass.nontrivial Subalgebra.instSubsemiringClass IsLocalRing.toNontrivial Field.instIsLocalRing Subalgebra.instIsTorsionFree FaithfulSMul.to_isTorsionFree Subsemiring.instFaithfulSMulSubtypeMem Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing instIsDomain
isIntegral_of_mem_ringOfIntegers 📖	mathematical	Subalgebra ValuationSubring SetLike.instMembership instSetLike Valuation.valuationSubring WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid CommRing.toCommSemiring instCommRingSubtypeMem CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instAlgebraSubtypeMemValuationSubringWithZeroMultiplicativeInt Subalgebra.instSetLike integralClosure	IsIntegral Subalgebra.toRing DivisionRing.toRing Field.toDivisionRing Subalgebra.algebra	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid integralClosure.isIntegral
isIntegral_of_mem_ringOfIntegers' 📖	mathematical	—	IsIntegral ValuationSubring SetLike.instMembership instSetLike Valuation.valuationSubring WithZero Multiplicative WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid Subalgebra CommRing.toCommSemiring instCommRingSubtypeMem CommSemiring.toSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain instAlgebraSubtypeMemValuationSubringWithZeroMultiplicativeInt Subalgebra.instSetLike integralClosure Subalgebra.toRing DivisionRing.toRing Field.toDivisionRing Subalgebra.algebra	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid isIntegral_of_mem_ringOfIntegers

---

← Back to Index