Basic

📁 Source: Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean

Statistics

Metric	Count
Definitions preΨ, preΨ', preΨ₄, Φ, Ψ, ΨSq, Ψ₂Sq, Ψ₃, φ, ψ, ψ₂	11
Theorems mk_Ψ_sq, mk_φ, mk_ψ, mk_ψ₂_sq, C_Ψ₂Sq, baseChange_preΨ, baseChange_preΨ', baseChange_preΨ₄, baseChange_Φ, baseChange_Ψ, baseChange_ΨSq, baseChange_Ψ₂Sq, baseChange_Ψ₃, baseChange_φ, baseChange_ψ, baseChange_ψ₂, map_preΨ, map_preΨ', map_preΨ₄, map_Φ, map_Ψ, map_ΨSq, map_Ψ₂Sq, map_Ψ₃, map_φ, map_ψ, map_ψ₂, preΨ'_even, preΨ'_four, preΨ'_odd, preΨ'_one, preΨ'_three, preΨ'_two, preΨ'_zero, preΨ_even, preΨ_four, preΨ_neg, preΨ_odd, preΨ_ofNat, preΨ_one, preΨ_three, preΨ_two, preΨ_zero, Φ_four, Φ_neg, Φ_ofNat, Φ_one, Φ_three, Φ_two, Φ_zero, ΨSq_even, ΨSq_four, ΨSq_neg, ΨSq_odd, ΨSq_ofNat, ΨSq_one, ΨSq_three, ΨSq_two, ΨSq_zero, Ψ_even, Ψ_four, Ψ_neg, Ψ_odd, Ψ_ofNat, Ψ_one, Ψ_three, Ψ_two, Ψ_zero, Ψ₂Sq_eq, φ_four, φ_neg, φ_one, φ_three, φ_two, φ_zero, ψ_even, ψ_four, ψ_neg, ψ_odd, ψ_one, ψ_three, ψ_two, ψ_zero, ψ₂_sq	84
Total	95

WeierstrassCurve

Definitions

Name	Category	Theorems
preΨ 📖	CompOp	19 math math: ΨSq_even, baseChange_preΨ, ΨSq_odd, preΨ_odd, preΨ_three, coeff_preΨ, natDegree_preΨ_pos, leadingCoeff_preΨ, preΨ_zero, preΨ_ofNat, natDegree_preΨ_le, map_preΨ, preΨ_neg, preΨ_four, preΨ_two, preΨ_one, Ψ_odd, preΨ_even, natDegree_preΨ
preΨ' 📖	CompOp	18 math math: coeff_preΨ', leadingCoeff_preΨ', preΨ'_zero, preΨ'_one, ΨSq_ofNat, baseChange_preΨ', preΨ'_even, Ψ_ofNat, natDegree_preΨ'_pos, preΨ'_three, map_preΨ', preΨ_ofNat, Φ_ofNat, preΨ'_odd, natDegree_preΨ', natDegree_preΨ'_le, preΨ'_two, preΨ'_four
preΨ₄ 📖	CompOp	16 math math: baseChange_preΨ₄, leadingCoeff_preΨ₄, natDegree_preΨ₄_pos, φ_three, natDegree_preΨ₄, Φ_three, natDegree_preΨ₄_le, coeff_preΨ₄, Φ_four, map_preΨ₄, φ_four, Ψ_four, preΨ_four, ΨSq_four, ψ_four, preΨ'_four
Φ 📖	CompOp	15 math math: natDegree_Φ_le, coeff_Φ, baseChange_Φ, map_Φ, natDegree_Φ, Affine.CoordinateRing.mk_φ, Φ_ofNat, Φ_three, Φ_four, leadingCoeff_Φ, Φ_two, Φ_neg, Φ_one, Φ_zero, natDegree_Φ_pos
Ψ 📖	CompOp	13 math math: map_Ψ, Ψ_one, Affine.CoordinateRing.mk_ψ, Ψ_ofNat, Ψ_neg, Ψ_three, Affine.CoordinateRing.mk_Ψ_sq, baseChange_Ψ, Ψ_even, Ψ_zero, Ψ_two, Ψ_four, Ψ_odd
ΨSq 📖	CompOp	17 math math: baseChange_ΨSq, ΨSq_even, ΨSq_odd, natDegree_ΨSq, ΨSq_ofNat, natDegree_ΨSq_le, natDegree_ΨSq_pos, Affine.CoordinateRing.mk_Ψ_sq, map_ΨSq, ΨSq_one, ΨSq_zero, leadingCoeff_ΨSq, ΨSq_two, ΨSq_neg, ΨSq_three, ΨSq_four, coeff_ΨSq
Ψ₂Sq 📖	CompOp	21 math math: coeff_Ψ₂Sq, map_Ψ₂Sq, ΨSq_even, ψ₂_sq, ΨSq_odd, baseChange_Ψ₂Sq, preΨ_odd, ΨSq_ofNat, leadingCoeff_Ψ₂Sq, natDegree_Ψ₂Sq_pos, C_Ψ₂Sq, Ψ₂Sq_eq, Φ_ofNat, Φ_three, preΨ'_odd, Φ_four, Affine.CoordinateRing.mk_ψ₂_sq, ΨSq_two, natDegree_Ψ₂Sq, ΨSq_four, natDegree_Ψ₂Sq_le
Ψ₃ 📖	CompOp	17 math math: preΨ_three, φ_three, preΨ'_three, Ψ_three, Φ_three, Φ_four, natDegree_Ψ₃_le, natDegree_Ψ₃_pos, natDegree_Ψ₃, ψ_three, map_Ψ₃, φ_four, coeff_Ψ₃, φ_two, ΨSq_three, baseChange_Ψ₃, leadingCoeff_Ψ₃
φ 📖	CompOp	9 math math: map_φ, φ_three, φ_neg, φ_one, baseChange_φ, Affine.CoordinateRing.mk_φ, φ_four, φ_two, φ_zero
ψ 📖	CompOp	11 math math: Affine.CoordinateRing.mk_ψ, ψ_two, ψ_even, ψ_zero, ψ_one, ψ_odd, ψ_three, ψ_neg, baseChange_ψ, map_ψ, ψ_four
ψ₂ 📖	CompOp	16 math math: map_ψ₂, ψ₂_sq, φ_three, baseChange_ψ₂, Ψ_ofNat, ψ_two, C_Ψ₂Sq, ψ_even, Ψ_even, Affine.CoordinateRing.mk_ψ₂_sq, φ_four, Ψ_two, Ψ_four, φ_two, ψ_four, Ψ_odd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_Ψ₂Sq 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Ψ₂Sq Polynomial.instSub Polynomial.ring CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ψ₂ Polynomial.instMul instOfNatAtLeastTwo Polynomial.instNatCast Nat.instAtLeastTwoHAddOfNat Affine.polynomial toAffine	—	Nat.instAtLeastTwoHAddOfNat Ψ₂Sq.eq_1 ψ₂.eq_1 b₂.eq_1 b₄.eq_1 b₆.eq_1 Affine.polynomialY.eq_1 Affine.polynomial.eq_1 map_ofNat RingHom.instRingHomClass Polynomial.C_add Polynomial.C_pow Polynomial.C_mul 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.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add
baseChange_preΨ 📖	mathematical	—	preΨ baseChange Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_preΨ map_baseChange
baseChange_preΨ' 📖	mathematical	—	preΨ' baseChange Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_preΨ' map_baseChange
baseChange_preΨ₄ 📖	mathematical	—	preΨ₄ baseChange Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_preΨ₄ map_baseChange
baseChange_Φ 📖	mathematical	—	Φ baseChange Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_Φ map_baseChange
baseChange_Ψ 📖	mathematical	—	Ψ baseChange Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_Ψ map_baseChange
baseChange_ΨSq 📖	mathematical	—	ΨSq baseChange Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_ΨSq map_baseChange
baseChange_Ψ₂Sq 📖	mathematical	—	Ψ₂Sq baseChange Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_Ψ₂Sq map_baseChange
baseChange_Ψ₃ 📖	mathematical	—	Ψ₃ baseChange Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_Ψ₃ map_baseChange
baseChange_φ 📖	mathematical	—	φ baseChange Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_φ map_baseChange
baseChange_ψ 📖	mathematical	—	ψ baseChange Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_ψ map_baseChange
baseChange_ψ₂ 📖	mathematical	—	ψ₂ baseChange Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass map_ψ₂ map_baseChange
map_preΨ 📖	mathematical	—	preΨ map Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring	—	map_Ψ₂Sq map_Ψ₃ map_preΨ₄ map_preNormEDS map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
map_preΨ' 📖	mathematical	—	preΨ' map Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring	—	map_Ψ₂Sq map_Ψ₃ map_preΨ₄ map_preNormEDS' map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
map_preΨ₄ 📖	mathematical	—	preΨ₄ map Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring	—	map_b₂ map_b₄ map_b₆ map_b₈ map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Polynomial.map_add Polynomial.map_mul Polynomial.map_ofNat Polynomial.map_pow Polynomial.map_X Polynomial.map_C Polynomial.map_sub
map_Φ 📖	mathematical	—	Φ map Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring	—	Polynomial.coe_mapRingHom map_ΨSq map_preΨ map_Ψ₂Sq mul_ite mul_one map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Polynomial.map_mul Polynomial.map_X
map_Ψ 📖	mathematical	—	Ψ map Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom	—	Polynomial.coe_mapRingHom map_preΨ map_ψ₂ mul_ite mul_one Polynomial.map_mul Polynomial.map_C
map_ΨSq 📖	mathematical	—	ΨSq map Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring	—	map_preΨ map_Ψ₂Sq mul_ite mul_one map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
map_Ψ₂Sq 📖	mathematical	—	Ψ₂Sq map Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring	—	map_ofNat RingHom.instRingHomClass map_b₂ map_b₄ map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_b₆ Polynomial.map_add Polynomial.map_mul Polynomial.map_ofNat Polynomial.map_pow Polynomial.map_X Polynomial.map_C
map_Ψ₃ 📖	mathematical	—	Ψ₃ map Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring	—	map_b₂ map_b₄ map_b₆ map_b₈ Polynomial.map_add Polynomial.map_mul Polynomial.map_ofNat Polynomial.map_pow Polynomial.map_X Polynomial.map_C
map_φ 📖	mathematical	—	φ map Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom	—	map_ψ Polynomial.map_sub Polynomial.map_mul Polynomial.map_C Polynomial.map_X Polynomial.map_pow
map_ψ 📖	mathematical	—	ψ map Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom	—	Polynomial.coe_mapRingHom map_ψ₂ map_Ψ₃ map_preΨ₄ map_normEDS Polynomial.map_C
map_ψ₂ 📖	mathematical	—	ψ₂ map Polynomial.map Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.mapRingHom	—	Affine.map_polynomialY
preΨ'_even 📖	mathematical	—	preΨ' Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instSub CommRing.toRing Polynomial.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	—	preNormEDS'_even
preΨ'_four 📖	mathematical	—	preΨ' preΨ₄	—	preNormEDS'_four
preΨ'_odd 📖	mathematical	—	preΨ' Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instSub CommRing.toRing Polynomial.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Even Nat.instDecidablePredEven Ψ₂Sq Polynomial.instOne	—	preNormEDS'_odd
preΨ'_one 📖	mathematical	—	preΨ' Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instOne	—	preNormEDS'_one
preΨ'_three 📖	mathematical	—	preΨ' Ψ₃	—	preNormEDS'_three
preΨ'_two 📖	mathematical	—	preΨ' Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instOne	—	preNormEDS'_two
preΨ'_zero 📖	mathematical	—	preΨ' Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instZero	—	preNormEDS'_zero
preΨ_even 📖	mathematical	—	preΨ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instSub CommRing.toRing Polynomial.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	—	preNormEDS_even
preΨ_four 📖	mathematical	—	preΨ preΨ₄	—	preNormEDS_four
preΨ_neg 📖	mathematical	—	preΨ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instNeg CommRing.toRing	—	preNormEDS_neg
preΨ_odd 📖	mathematical	—	preΨ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instSub CommRing.toRing Polynomial.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Even Int.instDecidablePredEven Ψ₂Sq Polynomial.instOne	—	preNormEDS_odd
preΨ_ofNat 📖	mathematical	—	preΨ preΨ'	—	preNormEDS_ofNat
preΨ_one 📖	mathematical	—	preΨ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instOne	—	preNormEDS_one
preΨ_three 📖	mathematical	—	preΨ Ψ₃	—	preNormEDS_three
preΨ_two 📖	mathematical	—	preΨ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instOne	—	preNormEDS_two
preΨ_zero 📖	mathematical	—	preΨ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instZero	—	preNormEDS_zero
Φ_four 📖	mathematical	—	Φ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instSub CommRing.toRing Polynomial.instMul Polynomial.X Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring preΨ₄ Ψ₂Sq Ψ₃	—	Φ_ofNat preΨ'_four preΨ'_odd preΨ'_two Even.zero preΨ'_one preΨ'_three Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat
Φ_neg 📖	mathematical	—	Φ	—	ΨSq_neg sub_neg_eq_add preΨ_neg neg_mul_neg mul_comm
Φ_ofNat 📖	mathematical	—	Φ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instSub CommRing.toRing Polynomial.instMul Polynomial.X Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring preΨ' Even Nat.instDecidablePredEven Polynomial.instOne Ψ₂Sq	—	Φ.eq_1 add_sub_cancel_right Nat.cast_one ΨSq_ofNat preΨ_ofNat
Φ_one 📖	mathematical	—	Φ Polynomial.X CommSemiring.toSemiring CommRing.toCommSemiring	—	ΨSq_one mul_one preΨ_two sub_self preΨ_zero MulZeroClass.mul_zero MulZeroClass.zero_mul sub_zero
Φ_three 📖	mathematical	—	Φ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instSub CommRing.toRing Polynomial.instMul Polynomial.X Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Ψ₃ preΨ₄ Ψ₂Sq	—	Φ_ofNat preΨ'_three mul_one preΨ'_four preΨ'_two Nat.instAtLeastTwoHAddOfNat even_two
Φ_two 📖	mathematical	—	Φ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instSub CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C b₄ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat b₆ b₈	—	Nat.instAtLeastTwoHAddOfNat Φ_ofNat preΨ'_two Nat.not_even_one Ψ₂Sq.eq_1 preΨ'_three preΨ'_one Ψ₃.eq_1 map_ofNat RingHom.instRingHomClass Polynomial.C_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat
Φ_zero 📖	mathematical	—	Φ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instOne	—	ΨSq_zero MulZeroClass.mul_zero zero_add preΨ_one zero_sub preΨ_neg mul_neg mul_one sub_neg_eq_add
ΨSq_even 📖	mathematical	—	ΨSq Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub CommRing.toRing preΨ Ψ₂Sq	—	ΨSq.eq_1 preΨ_even Nat.instAtLeastTwoHAddOfNat even_two_mul
ΨSq_four 📖	mathematical	—	ΨSq Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring preΨ₄ Ψ₂Sq	—	preΨ_four mul_ite mul_one instIsEmptyFalse
ΨSq_neg 📖	mathematical	—	ΨSq	—	preΨ_neg Even.neg_pow Nat.instAtLeastTwoHAddOfNat mul_ite mul_one
ΨSq_odd 📖	mathematical	—	ΨSq Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub CommRing.toRing Polynomial.instMul preΨ Even Int.instDecidablePredEven Ψ₂Sq Polynomial.instOne	—	ΨSq.eq_1 preΨ_odd Int.not_even_two_mul_add_one mul_one
ΨSq_ofNat 📖	mathematical	—	ΨSq Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring preΨ' Even Nat.instDecidablePredEven Ψ₂Sq Polynomial.instOne	—	preΨ_ofNat mul_ite mul_one
ΨSq_one 📖	mathematical	—	ΨSq Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instOne	—	preΨ_one one_pow mul_one
ΨSq_three 📖	mathematical	—	ΨSq Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Ψ₃	—	preΨ_three mul_one
ΨSq_two 📖	mathematical	—	ΨSq Ψ₂Sq	—	preΨ_two one_pow one_mul
ΨSq_zero 📖	mathematical	—	ΨSq Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instZero	—	preΨ_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.zero_mul
Ψ_even 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instMul Ψ ψ₂ Polynomial.instSub Polynomial.ring CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	preΨ_even Nat.instAtLeastTwoHAddOfNat even_two_mul Polynomial.C_sub Polynomial.C_mul Polynomial.C_pow Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Nat.cast_one
Ψ_four 📖	mathematical	—	Ψ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C preΨ₄ ψ₂	—	preΨ_four mul_ite mul_one instIsEmptyFalse
Ψ_neg 📖	mathematical	—	Ψ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instNeg Polynomial.ring CommRing.toRing	—	preΨ_neg Polynomial.C_neg neg_mul
Ψ_odd 📖	mathematical	—	Ψ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instAdd Polynomial.instSub Polynomial.ring CommRing.toRing Polynomial.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Affine.polynomial toAffine instOfNatAtLeastTwo Polynomial.instNatCast Nat.instAtLeastTwoHAddOfNat ψ₂ DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Even Int.instDecidablePredEven preΨ Polynomial.instNeg	—	Nat.instAtLeastTwoHAddOfNat preΨ_odd Int.not_even_two_mul_add_one Polynomial.C_sub Polynomial.C_mul Polynomial.C_pow C_Ψ₂Sq Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Nat.cast_one Mathlib.Tactic.Ring.add_congr Polynomial.C_neg Mathlib.Tactic.Ring.neg_congr
Ψ_ofNat 📖	mathematical	—	Ψ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C preΨ' Even Nat.instDecidablePredEven ψ₂ Polynomial.instOne	—	preΨ_ofNat mul_ite mul_one
Ψ_one 📖	mathematical	—	Ψ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instOne	—	preΨ_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mul_one
Ψ_three 📖	mathematical	—	Ψ DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Ψ₃	—	preΨ_three mul_one
Ψ_two 📖	mathematical	—	Ψ ψ₂	—	preΨ_two map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass one_mul
Ψ_zero 📖	mathematical	—	Ψ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instZero	—	preΨ_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul
Ψ₂Sq_eq 📖	mathematical	—	Ψ₂Sq Cubic.toPoly CommSemiring.toSemiring CommRing.toCommSemiring twoTorsionPolynomial	—	—
φ_four 📖	mathematical	—	φ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instAdd Polynomial.instSub Polynomial.ring CommRing.toRing Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Polynomial.X Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero preΨ₄ ψ₂ Ψ₃	—	φ.eq_1 ψ_four ψ_odd Nat.instAtLeastTwoHAddOfNat two_add_two_eq_four ψ_two ψ_one two_add_one_eq_three ψ_three Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Nat.cast_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_congr
φ_neg 📖	mathematical	—	φ	—	ψ_neg neg_sq sub_neg_eq_add neg_mul_neg mul_comm
φ_one 📖	mathematical	—	φ DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Polynomial.X	—	ψ_one one_pow mul_one ψ_two sub_self ψ_zero MulZeroClass.mul_zero sub_zero
φ_three 📖	mathematical	—	φ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instSub Polynomial.ring CommRing.toRing Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Polynomial.X Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ψ₃ preΨ₄ ψ₂	—	ψ_three sq ψ_four ψ_two mul_assoc
φ_two 📖	mathematical	—	φ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instSub Polynomial.ring CommRing.toRing Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Polynomial.X Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ψ₂ Ψ₃	—	ψ_two ψ_three ψ_one mul_one
φ_zero 📖	mathematical	—	φ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instOne	—	ψ_zero zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero zero_add ψ_one zero_sub ψ_neg mul_neg mul_one sub_neg_eq_add
ψ_even 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instMul ψ ψ₂ Polynomial.instSub Polynomial.ring CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	normEDS_even
ψ_four 📖	mathematical	—	ψ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C preΨ₄ ψ₂	—	normEDS_four
ψ_neg 📖	mathematical	—	ψ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instNeg Polynomial.ring CommRing.toRing	—	normEDS_neg
ψ_odd 📖	mathematical	—	ψ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instSub Polynomial.ring CommRing.toRing Polynomial.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	normEDS_odd
ψ_one 📖	mathematical	—	ψ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instOne	—	normEDS_one
ψ_three 📖	mathematical	—	ψ DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Ψ₃	—	normEDS_three
ψ_two 📖	mathematical	—	ψ ψ₂	—	normEDS_two
ψ_zero 📖	mathematical	—	ψ Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.instZero	—	normEDS_zero
ψ₂_sq 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero ψ₂ Polynomial.instAdd DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Ψ₂Sq Polynomial.instMul instOfNatAtLeastTwo Polynomial.instNatCast Nat.instAtLeastTwoHAddOfNat Affine.polynomial toAffine	—	Nat.instAtLeastTwoHAddOfNat C_Ψ₂Sq sub_add_cancel

WeierstrassCurve.Affine.CoordinateRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_Ψ_sq 📖	mathematical	—	WeierstrassCurve.Affine.CoordinateRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot.instCommRing Polynomial Polynomial.commRing WeierstrassCurve.Affine.polynomial DFunLike.coe RingHom Polynomial.semiring Semiring.toNonAssocSemiring RingHom.instFunLike WeierstrassCurve.Ψ Polynomial.C WeierstrassCurve.ΨSq	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_pow ite_pow mk_ψ₂_sq map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass one_pow map_pow
mk_φ 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring WeierstrassCurve.Affine.CoordinateRing Semiring.toNonAssocSemiring AdjoinRoot.instCommRing Polynomial.commRing WeierstrassCurve.Affine.polynomial RingHom.instFunLike WeierstrassCurve.φ Polynomial.C WeierstrassCurve.Φ	—	map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass mk_ψ mk_Ψ_sq mul_mul_mul_comm ite_pow map_one MonoidHomClass.toOneHomClass one_pow mk_ψ₂_sq
mk_ψ 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring WeierstrassCurve.Affine.CoordinateRing Semiring.toNonAssocSemiring AdjoinRoot.instCommRing Polynomial.commRing WeierstrassCurve.Affine.polynomial RingHom.instFunLike WeierstrassCurve.ψ WeierstrassCurve.Ψ	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_preNormEDS map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
mk_ψ₂_sq 📖	mathematical	—	WeierstrassCurve.Affine.CoordinateRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot.instCommRing Polynomial Polynomial.commRing WeierstrassCurve.Affine.polynomial DFunLike.coe RingHom Polynomial.semiring Semiring.toNonAssocSemiring RingHom.instFunLike WeierstrassCurve.ψ₂ Polynomial.C WeierstrassCurve.Ψ₂Sq	—	Nat.instAtLeastTwoHAddOfNat WeierstrassCurve.C_Ψ₂Sq map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass AdjoinRoot.mk_self MulZeroClass.mul_zero sub_zero

---

← Back to Index