Documentation Verification Report

Reduction

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

Statistics

Metric	Count
Definitions `IsGoodReduction`, `IsMinimal`, `integralModel`, `minimal`, `reduction`, `valuation_Δ_aux`	6
Theorems `goodReduction`, `integral`, `val_Δ_maximal`, `baseChange_integralModel_eq`, `exists_isIntegral`, `exists_isMinimal`, `instIsIntegralOfIsMinimal`, `instIsMinimalMinimal`, `integralModel_Δ_eq`, `isGoodReduction_iff`, `isGoodReduction_iff_isElliptic_reduction`, `isIntegral_iff`, `isIntegral_of_exists_lift`, `isMinimal_iff`, `valuation_Δ_aux_eq_of_isIntegral`, `Δ_integral_of_isIntegral`	16
Total	22

WeierstrassCurve

Definitions

Name	Category	Theorems
`IsGoodReduction` 📖	CompData	2 math math: `isGoodReduction_iff`, `isGoodReduction_iff_isElliptic_reduction`
`IsMinimal` 📖	CompData	3 math math: `exists_isMinimal`, `instIsMinimalMinimal`, `isMinimal_iff`
`integralModel` 📖	CompOp	2 math math: `integralModel_Δ_eq`, `baseChange_integralModel_eq`
`minimal` 📖	CompOp	1 math math: `instIsMinimalMinimal`
`reduction` 📖	CompOp	1 math math: `isGoodReduction_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	—	`IsIntegral` `VariableChange` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `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	—	`IsMinimal` `VariableChange` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `WeierstrassCurve` `instSMulVariableChange`	—	`exists_maximalFor_of_wellFoundedGT` `instWellFoundedGTWithZeroMultiplicativeIntLeOne` `exists_isIntegral` `of_isDiscreteValuationRing` `one_smul` `smul_assoc` `IsScalarTower.left` `valuation_Δ_aux.congr_simp`
`instIsIntegralOfIsMinimal` 📖	mathematical	—	`IsIntegral`	—	`one_smul` `IsMinimal.val_Δ_maximal`
`instIsMinimalMinimal` 📖	mathematical	—	`IsMinimal` `minimal`	—	`exists_isMinimal`
`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` 📖	mathematical	—	`IsGoodReduction` `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` `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`
`isGoodReduction_iff_isElliptic_reduction` 📖	mathematical	—	`IsGoodReduction` `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` `isGoodReduction_iff` `integralModel_Δ_eq` `LE.le.ge_iff_eq` `IsDedekindDomain.HeightOneSpectrum.valuation_le_one` `isElliptic_iff`
`isIntegral_iff` 📖	mathematical	—	`IsIntegral` `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.IsGoodReduction

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` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `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`	—	—

WeierstrassCurve.IsIntegral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral` 📖	mathematical	—	`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