SInteger

📁 Source: Mathlib/RingTheory/DedekindDomain/SInteger.lean

Statistics

Metric	Count
Definitions integer, unit, unitEquivUnitsInteger	3
Theorems integer_empty, integer_univ, coe_integer, coe_unit, integer_eq, integer_valuation_le_one, unitEquivUnitsInteger_symm_apply_coe, unit_eq, unit_valuation_eq_one, val_unitEquivUnitsInteger_apply_coe	10
Total	13

IsDedekindDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integer_empty 📖	mathematical	—	Set.integer Set HeightOneSpectrum Set.instEmptyCollection Bot.bot Subalgebra CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	Subalgebra.ext iInf_congr_Prop HeightOneSpectrum.valuation_le_one Subring.copy.congr_simp HeightOneSpectrum.mem_integers_of_valuation_le_one
integer_univ 📖	mathematical	—	Set.integer Set.univ HeightOneSpectrum Top.top Subalgebra CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Subalgebra.ext

Set

Definitions

Name	Category	Theorems
integer 📖	CompOp	7 math math: unitEquivUnitsInteger_symm_apply_coe, IsDedekindDomain.integer_empty, coe_integer, val_unitEquivUnitsInteger_apply_coe, integer_valuation_le_one, integer_eq, IsDedekindDomain.integer_univ
unit 📖	CompOp	5 math math: unit_eq, unitEquivUnitsInteger_symm_apply_coe, coe_unit, val_unitEquivUnitsInteger_apply_coe, unit_valuation_eq_one
unitEquivUnitsInteger 📖	CompOp	2 math math: unitEquivUnitsInteger_symm_apply_coe, val_unitEquivUnitsInteger_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_integer 📖	mathematical	—	SetLike.coe Subalgebra CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subalgebra.instSetLike integer setOf	—	—
coe_unit 📖	mathematical	—	SetLike.coe Subgroup Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Units.instGroup Subgroup.instSetLike unit setOf	—	—
integer_eq 📖	mathematical	—	Subalgebra.toSubring DivisionRing.toRing Field.toDivisionRing integer iInf Subring IsDedekindDomain.HeightOneSpectrum Subring.instInfSet Set instMembership ValuationSubring.toSubring 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 IsDedekindDomain.HeightOneSpectrum.valuation	—	SetLike.ext' Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid ext Subring.coe_iInf
integer_valuation_le_one 📖	mathematical	IsDedekindDomain.HeightOneSpectrum Set instMembership	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt DFunLike.coe Valuation WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.valuation Subalgebra CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SetLike.instMembership Subalgebra.instSetLike integer WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—
unitEquivUnitsInteger_symm_apply_coe 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unit DFunLike.coe MulEquiv Subalgebra CommRing.toCommSemiring Subalgebra.instSetLike integer Subalgebra.toSemiring Units.instMul Subgroup.mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm unitEquivUnitsInteger DivisionSemiring.toGroupWithZero Units.val	—	—
unit_eq 📖	mathematical	—	unit iInf Subgroup Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Units.instGroup IsDedekindDomain.HeightOneSpectrum Subgroup.instInfSet Set instMembership ValuationSubring.unitGroup 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 IsDedekindDomain.HeightOneSpectrum.valuation	—	Subgroup.copy_eq
unit_valuation_eq_one 📖	mathematical	IsDedekindDomain.HeightOneSpectrum Set instMembership	DFunLike.coe Valuation 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 Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.valuation Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Units Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike unit WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—
val_unitEquivUnitsInteger_apply_coe 📖	mathematical	—	Subalgebra CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SetLike.instMembership Subalgebra.instSetLike integer Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Subalgebra.toSemiring DFunLike.coe MulEquiv Units Subgroup Units.instGroup Subgroup.instSetLike unit Subgroup.mul Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike unitEquivUnitsInteger	—	—

---

← Back to Index