Reduction

📁 Source: Mathlib/AlgebraicGeometry/EllipticCurve/Reduction.lean

Statistics

Metric	Count
Definitions HasAdditiveReduction, HasGoodReduction, HasMultiplicativeReduction, IsGoodReduction, IsMinimal, integralModel, minimal, reduction, valuation_Δ_aux	9
Theorems additiveReduction, badReduction, not_hasGoodReduction, not_hasMultiplicativeReduction, toIsMinimal, goodReduction, not_hasAdditiveReduction, not_hasMultiplicativeReduction, toIsMinimal, badReduction, multiplicativeReduction, not_hasAdditiveReduction, not_hasGoodReduction, toIsMinimal, integral, val_Δ_maximal, baseChange_integralModel_eq, exists_isIntegral, exists_isMinimal, hasAdditiveReduction_iff, hasGoodReduction_iff, hasGoodReduction_iff_isElliptic_reduction, hasGoodReduction_or_hasMultiplicativeReduction_or_hasAdditiveReduction, hasMultiplicativeReduction_iff, instIsIntegralOfIsMinimal, instIsMinimalMinimal, integralModel_a₁_eq, integralModel_a₂_eq, integralModel_a₃_eq, integralModel_a₄_eq, integralModel_a₆_eq, integralModel_b₂_eq, integralModel_b₄_eq, integralModel_b₆_eq, integralModel_b₈_eq, integralModel_c₄_eq, integralModel_c₆_eq, integralModel_Δ_eq, isGoodReduction_iff_isElliptic_reduction, isIntegral_iff, isIntegral_of_exists_lift, isMinimal_iff, valuation_Δ_aux_eq_of_isIntegral, Δ_integral_of_isIntegral	44
Total	53

WeierstrassCurve

Definitions

Name	Category	Theorems
HasAdditiveReduction 📖	CompData	4 math math: hasGoodReduction_or_hasMultiplicativeReduction_or_hasAdditiveReduction, hasAdditiveReduction_iff, HasGoodReduction.not_hasAdditiveReduction, HasMultiplicativeReduction.not_hasAdditiveReduction
HasGoodReduction 📖	CompData	6 math math: HasAdditiveReduction.not_hasGoodReduction, hasGoodReduction_iff, HasMultiplicativeReduction.not_hasGoodReduction, hasGoodReduction_or_hasMultiplicativeReduction_or_hasAdditiveReduction, isGoodReduction_iff_isElliptic_reduction, hasGoodReduction_iff_isElliptic_reduction
HasMultiplicativeReduction 📖	CompData	4 math math: HasGoodReduction.not_hasMultiplicativeReduction, hasMultiplicativeReduction_iff, hasGoodReduction_or_hasMultiplicativeReduction_or_hasAdditiveReduction, HasAdditiveReduction.not_hasMultiplicativeReduction
IsGoodReduction 📖	MathDef	—
IsMinimal 📖	CompData	9 math math: exists_isMinimal, hasGoodReduction_iff, hasMultiplicativeReduction_iff, instIsMinimalMinimal, HasAdditiveReduction.toIsMinimal, hasAdditiveReduction_iff, isMinimal_iff, HasMultiplicativeReduction.toIsMinimal, HasGoodReduction.toIsMinimal
integralModel 📖	CompOp	13 math math: integralModel_b₆_eq, integralModel_Δ_eq, integralModel_b₂_eq, integralModel_a₄_eq, integralModel_a₁_eq, baseChange_integralModel_eq, integralModel_a₂_eq, integralModel_c₆_eq, integralModel_c₄_eq, integralModel_b₄_eq, integralModel_b₈_eq, integralModel_a₃_eq, integralModel_a₆_eq
minimal 📖	CompOp	1 math math: instIsMinimalMinimal
reduction 📖	CompOp	2 math math: isGoodReduction_iff_isElliptic_reduction, hasGoodReduction_iff_isElliptic_reduction
valuation_Δ_aux 📖	CompOp	3 math math: valuation_Δ_aux_eq_of_isIntegral, IsMinimal.val_Δ_maximal, isMinimal_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
baseChange_integralModel_eq 📖	mathematical	—	baseChange integralModel EuclideanDomain.toCommRing Field.toEuclideanDomain	—	IsIntegral.integral
exists_isIntegral 📖	mathematical	—	VariableChange EuclideanDomain.toCommRing Field.toEuclideanDomain IsIntegral WeierstrassCurve instSMulVariableChange	—	zero_add IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Nat.instAtLeastTwoHAddOfNat List.maximum_of_length_pos_mem List.le_maximum_of_length_pos_of_mem isIntegral_of_exists_lift inv_one MulZeroClass.mul_zero add_zero one_mul one_pow MulZeroClass.zero_mul sub_zero zero_pow Nat.instCharZero LE.le.trans le_of_not_ge instLawfulBCmpCompare_mathlib map_zero MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass zero_le_one LinearOrderedCommMonoidWithZero.toZeroLeOneClass ValuationRing.mem_integer_iff Units.val_inv_eq_inv_val inv_pow Valuation.mem_integer_iff map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass map_inv₀ inv_mul_le_one_of_le₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE LinearOrderedCommMonoidWithZero.toPosMulStrictMono le_refl zero_le' map_pow le_self_pow IsOrderedMonoid.toMulLeftMono LinearOrderedCommMonoidWithZero.toIsOrderedMonoid GE.ge.le Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.mul_neg Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true Int.instCharZero sub_eq_zero_of_eq Nat.cast_zero
exists_isMinimal 📖	mathematical	—	VariableChange EuclideanDomain.toCommRing Field.toEuclideanDomain IsMinimal WeierstrassCurve instSMulVariableChange	—	exists_maximalFor_of_wellFoundedGT instWellFoundedGTWithZeroMultiplicativeIntLeOne exists_isIntegral of_isDiscreteValuationRing one_smul smul_assoc IsScalarTower.left valuation_Δ_aux.congr_simp
hasAdditiveReduction_iff 📖	mathematical	—	HasAdditiveReduction IsMinimal WithZero Multiplicative Preorder.toLT 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 IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing IsDiscreteValuationRing.maximalIdeal Δ EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing c₄	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing
hasGoodReduction_iff 📖	mathematical	—	HasGoodReduction IsMinimal DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring instLatticeInt Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.valuation IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing IsDiscreteValuationRing.maximalIdeal Δ EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing
hasGoodReduction_iff_isElliptic_reduction 📖	mathematical	—	HasGoodReduction IsElliptic IsLocalRing.ResidueField IsDiscreteValuationRing.toIsLocalRing IsLocalRing.instCommRingResidueField reduction	—	IsDiscreteValuationRing.toIsLocalRing instIsIntegralOfIsMinimal map_Δ Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing not_iff_not IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem hasGoodReduction_iff integralModel_Δ_eq LE.le.ge_iff_eq IsDedekindDomain.HeightOneSpectrum.valuation_le_one isElliptic_iff
hasGoodReduction_or_hasMultiplicativeReduction_or_hasAdditiveReduction 📖	mathematical	—	HasGoodReduction HasMultiplicativeReduction HasAdditiveReduction	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing hasGoodReduction_iff hasMultiplicativeReduction_iff hasAdditiveReduction_iff instIsIntegralOfIsMinimal integralModel_Δ_eq integralModel_c₄_eq
hasMultiplicativeReduction_iff 📖	mathematical	—	HasMultiplicativeReduction IsMinimal WithZero Multiplicative Preorder.toLT 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 IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing IsDiscreteValuationRing.maximalIdeal Δ EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing c₄	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing
instIsIntegralOfIsMinimal 📖	mathematical	—	IsIntegral	—	one_smul IsMinimal.val_Δ_maximal
instIsMinimalMinimal 📖	mathematical	—	IsMinimal minimal	—	exists_isMinimal
integralModel_a₁_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap a₁ integralModel	—	baseChange_integralModel_eq IsIntegral.integral
integralModel_a₂_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap a₂ integralModel	—	baseChange_integralModel_eq IsIntegral.integral
integralModel_a₃_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap a₃ integralModel	—	baseChange_integralModel_eq IsIntegral.integral
integralModel_a₄_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap a₄ integralModel	—	baseChange_integralModel_eq IsIntegral.integral
integralModel_a₆_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap a₆ integralModel	—	baseChange_integralModel_eq IsIntegral.integral
integralModel_b₂_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap b₂ integralModel EuclideanDomain.toCommRing Field.toEuclideanDomain	—	baseChange_integralModel_eq IsIntegral.integral map_b₂
integralModel_b₄_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap b₄ integralModel EuclideanDomain.toCommRing Field.toEuclideanDomain	—	baseChange_integralModel_eq IsIntegral.integral map_b₄
integralModel_b₆_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap b₆ integralModel EuclideanDomain.toCommRing Field.toEuclideanDomain	—	baseChange_integralModel_eq IsIntegral.integral map_b₆
integralModel_b₈_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap b₈ integralModel EuclideanDomain.toCommRing Field.toEuclideanDomain	—	baseChange_integralModel_eq IsIntegral.integral map_b₈
integralModel_c₄_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap c₄ integralModel EuclideanDomain.toCommRing Field.toEuclideanDomain	—	baseChange_integralModel_eq IsIntegral.integral map_c₄
integralModel_c₆_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap c₆ integralModel EuclideanDomain.toCommRing Field.toEuclideanDomain	—	baseChange_integralModel_eq IsIntegral.integral map_c₆
integralModel_Δ_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap Δ integralModel EuclideanDomain.toCommRing Field.toEuclideanDomain	—	baseChange_integralModel_eq IsIntegral.integral map_Δ
isGoodReduction_iff_isElliptic_reduction 📖	mathematical	—	HasGoodReduction IsElliptic IsLocalRing.ResidueField IsDiscreteValuationRing.toIsLocalRing IsLocalRing.instCommRingResidueField reduction	—	hasGoodReduction_iff_isElliptic_reduction
isIntegral_iff 📖	mathematical	—	IsIntegral WeierstrassCurve baseChange EuclideanDomain.toCommRing Field.toEuclideanDomain	—	—
isIntegral_of_exists_lift 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap a₁ a₂ a₃ a₄ a₆	IsIntegral	—	ext
isMinimal_iff 📖	mathematical	—	IsMinimal MaximalFor VariableChange EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing IsIntegral WeierstrassCurve instSMulVariableChange valuation_Δ_aux VariableChange.instOne	—	—
valuation_Δ_aux_eq_of_isIntegral 📖	mathematical	—	WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing valuation_Δ_aux 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 IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing IsDiscreteValuationRing.maximalIdeal Δ EuclideanDomain.toCommRing Field.toEuclideanDomain	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing
Δ_integral_of_isIntegral 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike algebraMap Δ EuclideanDomain.toCommRing Field.toEuclideanDomain	—	IsIntegral.integral map_Δ

WeierstrassCurve.HasAdditiveReduction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
additiveReduction 📖	mathematical	—	WithZero Multiplicative Preorder.toLT 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 IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing IsDiscreteValuationRing.maximalIdeal WeierstrassCurve.c₄ EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—
badReduction 📖	mathematical	—	WithZero Multiplicative Preorder.toLT 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 IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing IsDiscreteValuationRing.maximalIdeal WeierstrassCurve.Δ EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—
not_hasGoodReduction 📖	mathematical	—	WeierstrassCurve.HasGoodReduction	—	LT.lt.ne Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing badReduction WeierstrassCurve.HasGoodReduction.goodReduction
not_hasMultiplicativeReduction 📖	mathematical	—	WeierstrassCurve.HasMultiplicativeReduction	—	LT.lt.ne Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing additiveReduction WeierstrassCurve.HasMultiplicativeReduction.multiplicativeReduction
toIsMinimal 📖	mathematical	—	WeierstrassCurve.IsMinimal	—	—

WeierstrassCurve.HasGoodReduction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
goodReduction 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring instLatticeInt Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.valuation IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing IsDiscreteValuationRing.maximalIdeal WeierstrassCurve.Δ EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—
not_hasAdditiveReduction 📖	mathematical	—	WeierstrassCurve.HasAdditiveReduction	—	LT.lt.ne Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing WeierstrassCurve.HasAdditiveReduction.badReduction goodReduction
not_hasMultiplicativeReduction 📖	mathematical	—	WeierstrassCurve.HasMultiplicativeReduction	—	LT.lt.ne Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing WeierstrassCurve.HasMultiplicativeReduction.badReduction goodReduction
toIsMinimal 📖	mathematical	—	WeierstrassCurve.IsMinimal	—	—

WeierstrassCurve.HasMultiplicativeReduction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
badReduction 📖	mathematical	—	WithZero Multiplicative Preorder.toLT 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 IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing IsDiscreteValuationRing.maximalIdeal WeierstrassCurve.Δ EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—
multiplicativeReduction 📖	mathematical	—	DFunLike.coe Valuation WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring instLatticeInt Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.valuation IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing IsDiscreteValuationRing.maximalIdeal WeierstrassCurve.c₄ EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing	—	—
not_hasAdditiveReduction 📖	mathematical	—	WeierstrassCurve.HasAdditiveReduction	—	LT.lt.ne Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing WeierstrassCurve.HasAdditiveReduction.additiveReduction multiplicativeReduction
not_hasGoodReduction 📖	mathematical	—	WeierstrassCurve.HasGoodReduction	—	LT.lt.ne Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing IsPrincipalIdealRing.isDedekindDomain IsDiscreteValuationRing.toIsPrincipalIdealRing badReduction WeierstrassCurve.HasGoodReduction.goodReduction
toIsMinimal 📖	mathematical	—	WeierstrassCurve.IsMinimal	—	—

WeierstrassCurve.IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
integral 📖	mathematical	—	WeierstrassCurve WeierstrassCurve.baseChange EuclideanDomain.toCommRing Field.toEuclideanDomain	—	—

WeierstrassCurve.IsMinimal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
val_Δ_maximal 📖	mathematical	—	MaximalFor WeierstrassCurve.VariableChange EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative Preorder.toLE WithZero.instPreorder Multiplicative.preorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf instLatticeInt WithZero.one instOneMultiplicativeOfZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing WeierstrassCurve.IsIntegral WeierstrassCurve WeierstrassCurve.instSMulVariableChange WeierstrassCurve.valuation_Δ_aux WeierstrassCurve.VariableChange.instOne	—	—

---

← Back to Index