Integral

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

Statistics

Metric	Count
Definitions Integral	1
Theorems integralClosure, integrallyClosed, isIntegral_iff_v_le_one, isIntegrallyClosed, isIntegrallyClosed_integers, mem_of_integral	6
Total	7

MeasCat

Definitions

Name	Category	Theorems
Integral 📖	CompOp	—

Valuation.Integers

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integralClosure 📖	mathematical	Valuation.Integers	integralClosure Bot.bot Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	bot_unique exists_of_le_one mem_of_integral Algebra.mem_bot
integrallyClosed 📖	mathematical	Valuation.Integers EuclideanDomain.toCommRing Field.toEuclideanDomain	IsIntegrallyClosed	—	isIntegrallyClosed
isIntegral_iff_v_le_one 📖	mathematical	Valuation.Integers	IsIntegral CommRing.toRing Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation Valuation.instFunLike InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Module.IsNoetherian.finite isNoetherian_of_finite Finite.of_subsingleton nontrivial_iff Polynomial.natDegree_eq_zero Polynomial.eval₂_C map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.Monic.ne_zero_of_C Mathlib.Tactic.Contrapose.contrapose₁ ne_of_lt Valuation.map_sum_lt isReduced_of_noZeroDivisors GroupWithZero.noZeroDivisors LT.lt.ne' LT.lt.trans' zero_lt_one LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.one GroupWithZero.toNontrivial map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass map_pow mul_lt_of_le_one_of_lt covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono LinearOrderedCommMonoidWithZero.toIsOrderedMonoid map_le_one pow_lt_pow_right₀ LinearOrderedCommMonoidWithZero.toPosMulStrictMono Valuation.map_neg Polynomial.eval₂_eq_sum_range Finset.sum_range_succ Polynomial.Monic.coeff_natDegree map_one MonoidHomClass.toOneHomClass one_mul exists_of_le_one Polynomial.monic_of_natDegree_le_of_coeff_eq_one Polynomial.natDegree_sub_le_of_le Polynomial.natDegree_X_le Mathlib.Tactic.ComputeDegree.natDegree_C_le Mathlib.Tactic.ComputeDegree.coeff_congr Mathlib.Tactic.ComputeDegree.coeff_sub_of_eq Polynomial.coeff_X Polynomial.coeff_C sub_zero Polynomial.eval₂_sub Polynomial.eval₂_X sub_self
isIntegrallyClosed 📖	mathematical	Valuation.Integers EuclideanDomain.toCommRing Field.toEuclideanDomain	IsIntegrallyClosed	—	isFractionRing IsIntegrallyClosed.integralClosure_eq_bot_iff integralClosure
isIntegrallyClosed_integers 📖	mathematical	—	IsIntegrallyClosed Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike Valuation.integer Subring.toCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	isIntegrallyClosed Valuation.integer.integers
mem_of_integral 📖	mathematical	Valuation.Integers IsIntegral CommRing.toRing	Subring SetLike.instMembership Subring.instSetLike Valuation.integer	—	isIntegral_iff_v_le_one

---

← Back to Index