SelmerGroup

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

Statistics

Metric	Count
Definitions valuationOfNeZero, valuationOfNeZeroMod, valuationOfNeZeroToFun, selmerGroup, fromUnit, fromUnitLift, valuation	7
Theorems valuationOfNeZeroToFun_eq, valuationOfNeZero_eq, valuation_of_unit_eq, valuation_of_unit_mod_eq, fromUnitLift_injective, fromUnit_ker, monotone, valuation_ker_eq	8
Total	15

IsDedekindDomain

Definitions

Name	Category	Theorems
selmerGroup 📖	CompOp	4 math math: selmerGroup.monotone, selmerGroup.fromUnit_ker, selmerGroup.fromUnitLift_injective, selmerGroup.valuation_ker_eq

IsDedekindDomain.HeightOneSpectrum

Definitions

Name	Category	Theorems
valuationOfNeZero 📖	CompOp	2 math math: valuation_of_unit_eq, valuationOfNeZero_eq
valuationOfNeZeroMod 📖	CompOp	1 math math: valuation_of_unit_mod_eq
valuationOfNeZeroToFun 📖	CompOp	1 math math: valuationOfNeZeroToFun_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
valuationOfNeZeroToFun_eq 📖	mathematical	—	WithZero.coe Multiplicative valuationOfNeZeroToFun DFunLike.coe Valuation WithZero 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 valuation Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Units.val_inv_eq_inv_val Ideal.uniqueFactorizationMonoid IsLocalization.sec_fst_ne_zero Units.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing nonZeroDivisors.coe_ne_zero IsDomain.toNontrivial IsDedekindDomain.toIsDomain
valuationOfNeZero_eq 📖	mathematical	—	WithZero.coe Multiplicative DFunLike.coe MonoidHom Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulOneClass.toMulOne Units.instMulOneClass Multiplicative.mulOneClass AddMonoid.toAddZeroClass Int.instAddMonoid MonoidHom.instFunLike valuationOfNeZero Valuation WithZero 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 valuation Units.val	—	valuationOfNeZeroToFun_eq
valuation_of_unit_eq 📖	mathematical	—	DFunLike.coe MonoidHom Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Multiplicative MulOneClass.toMulOne Units.instMulOneClass Multiplicative.mulOneClass AddMonoid.toAddZeroClass Int.instAddMonoid MonoidHom.instFunLike valuationOfNeZero CommSemiring.toSemiring CommRing.toCommSemiring Units.map MonoidHomClass.toMonoidHom RingHom Semiring.toNonAssocSemiring MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing valuationOfNeZero_eq Units.coe_map eq_iff_le_not_lt valuation_le_one not_lt map_mul MonoidHomClass.toMulHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass map_one MonoidHomClass.toOneHomClass mul_one valuation_of_algebraMap mul_le_mul_right WithZero.instMulLeftMono IsOrderedMonoid.toMulLeftMono Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid intValuation_le_one
valuation_of_unit_mod_eq 📖	mathematical	—	DFunLike.coe MonoidHom HasQuotient.Quotient Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup Units.instGroup QuotientGroup.instHasQuotientSubgroup MonoidHom.range powMonoidHom CommGroup.toCommMonoid Units.instCommGroupUnits CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Multiplicative ZMod MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid QuotientGroup.Quotient.group Subgroup.normal_of_comm Multiplicative.mulOneClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing MonoidHom.instFunLike valuationOfNeZeroMod CommSemiring.toSemiring CommRing.toCommSemiring Units.instMulOneClass Units.map MonoidHomClass.toMonoidHom RingHom Semiring.toNonAssocSemiring MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Subgroup.normal_of_comm MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass valuationOfNeZeroMod.eq_1 MonoidHom.comp_apply QuotientGroup.coe_mk' QuotientGroup.map_mk' valuation_of_unit_eq QuotientGroup.mk_one map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass

IsDedekindDomain.selmerGroup

Definitions

Name	Category	Theorems
fromUnit 📖	CompOp	1 math math: fromUnit_ker
fromUnitLift 📖	CompOp	1 math math: fromUnitLift_injective
valuation 📖	CompOp	1 math math: valuation_ker_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fromUnitLift_injective 📖	mathematical	—	HasQuotient.Quotient Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Subgroup Units.instGroup QuotientGroup.instHasQuotientSubgroup MonoidHom.range powMonoidHom CommGroup.toCommMonoid Units.instCommGroupUnits CommRing.toCommMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield EuclideanDomain.toCommRing Field.toEuclideanDomain QuotientGroup.Quotient.group Subgroup.normal_of_comm SetLike.instMembership Subgroup.instSetLike IsDedekindDomain.selmerGroup Set IsDedekindDomain.HeightOneSpectrum Set.instEmptyCollection DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup MonoidHom.instFunLike fromUnitLift	—	Subgroup.normal_of_comm fromUnit_ker QuotientGroup.kerLift_injective MulEquiv.injective
fromUnit_ker 📖	mathematical	—	MonoidHom.ker Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup HasQuotient.Quotient DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup QuotientGroup.instHasQuotientSubgroup MonoidHom.range powMonoidHom CommGroup.toCommMonoid Units.instCommGroupUnits CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain QuotientGroup.Quotient.group Subgroup.normal_of_comm SetLike.instMembership Subgroup.instSetLike IsDedekindDomain.selmerGroup Set IsDedekindDomain.HeightOneSpectrum Set.instEmptyCollection Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Subgroup.toGroup fromUnit	—	Subgroup.ext Subgroup.normal_of_comm QuotientGroup.eq_one_iff IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq OneMemClass.one_mem Subgroup.instSubgroupClass IsIntegrallyClosed.exists_algebraMap_eq_of_isIntegral_pow IsDedekindRing.toIsIntegralClosure IsDedekindDomain.toIsDedekindRing Fact.out isIntegral_algebraMap Units.val_pow_eq_pow_val map_eq_one_iff MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass FaithfulSMul.algebraMap_injective IsFractionRing.instFaithfulSMul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Module.IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDedekindDomain.toIsDomain IsLocalRing.toNontrivial Field.instIsLocalRing FaithfulSMul.to_isTorsionFree IsDomain.toNontrivial instIsDomain map_pow inv_pow MonoidHom.instMonoidHomClass
monotone 📖	mathematical	Set IsDedekindDomain.HeightOneSpectrum Set.instLE	Subgroup HasQuotient.Quotient Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Units.instGroup QuotientGroup.instHasQuotientSubgroup MonoidHom.range powMonoidHom CommGroup.toCommMonoid Units.instCommGroupUnits CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain QuotientGroup.Quotient.group Subgroup.normal_of_comm Preorder.toLE PartialOrder.toPreorder Subgroup.instPartialOrder IsDedekindDomain.selmerGroup	—	Subgroup.normal_of_comm
valuation_ker_eq 📖	mathematical	—	MonoidHom.ker HasQuotient.Quotient Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subgroup Units.instGroup QuotientGroup.instHasQuotientSubgroup MonoidHom.range powMonoidHom CommGroup.toCommMonoid Units.instCommGroupUnits CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain QuotientGroup.Quotient.group Subgroup.normal_of_comm SetLike.instMembership Subgroup.instSetLike IsDedekindDomain.selmerGroup Subgroup.toGroup Pi.mulOneClass Set.Elem IsDedekindDomain.HeightOneSpectrum Multiplicative ZMod Multiplicative.mulOneClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ZMod.commRing valuation Subgroup.subgroupOf Set Set.instEmptyCollection	—	Subgroup.ext Subgroup.normal_of_comm Set.notMem_empty

---

← Back to Index