Degree

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

Statistics

Metric	Count
Definitions	0
Theorems coeff_preΨ, coeff_preΨ', coeff_preΨ'_ne_zero, coeff_preΨ_ne_zero, coeff_preΨ₄, coeff_preΨ₄_ne_zero, coeff_Φ, coeff_Φ_ne_zero, coeff_ΨSq, coeff_ΨSq_ne_zero, coeff_Ψ₂Sq, coeff_Ψ₂Sq_ne_zero, coeff_Ψ₃, coeff_Ψ₃_ne_zero, leadingCoeff_preΨ, leadingCoeff_preΨ', leadingCoeff_preΨ₄, leadingCoeff_Φ, leadingCoeff_ΨSq, leadingCoeff_Ψ₂Sq, leadingCoeff_Ψ₃, natDegree_preΨ, natDegree_preΨ', natDegree_preΨ'_le, natDegree_preΨ'_pos, natDegree_preΨ_le, natDegree_preΨ_pos, natDegree_preΨ₄, natDegree_preΨ₄_le, natDegree_preΨ₄_pos, natDegree_Φ, natDegree_Φ_le, natDegree_Φ_pos, natDegree_ΨSq, natDegree_ΨSq_le, natDegree_ΨSq_pos, natDegree_Ψ₂Sq, natDegree_Ψ₂Sq_le, natDegree_Ψ₂Sq_pos, natDegree_Ψ₃, natDegree_Ψ₃_le, natDegree_Ψ₃_pos, preΨ'_ne_zero, preΨ_ne_zero, preΨ₄_ne_zero, Φ_ne_zero, ΨSq_ne_zero, Ψ₂Sq_ne_zero, Ψ₃_ne_zero	49
Total	49

WeierstrassCurve

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_preΨ 📖	mathematical	—	Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring preΨ Monoid.toNatPow Nat.instMonoid Even Int.instDecidablePredEven AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	Int.cast_natCast coeff_preΨ' preΨ_ofNat preΨ_neg Polynomial.coeff_neg Nat.even_or_odd' Nat.instAtLeastTwoHAddOfNat Nat.cast_mul Int.cast_neg Nat.cast_add Nat.cast_one Int.cast_add Int.cast_mul Int.cast_ofNat Int.cast_one
coeff_preΨ' 📖	mathematical	—	Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring preΨ' Monoid.toNatPow Nat.instMonoid Even Nat.instDecidablePredEven AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Nat.even_or_odd' Distrib.rightDistribClass Nat.instAtLeastTwoHAddOfNat mul_div_cancel_left₀ Nat.instMulDivCancelClass Nat.instCharZero Nat.cast_mul Int.instMulDivCancelClass Int.instCharZero Int.cast_natCast Nat.not_even_two_mul_add_one Nat.cast_add Nat.cast_one Int.cast_add Int.cast_mul Int.cast_ofNat Int.cast_one
coeff_preΨ'_ne_zero 📖	—	—	—	—	Nat.even_or_odd' coeff_preΨ' Nat.instAtLeastTwoHAddOfNat even_two_mul two_pos Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid right_ne_zero_of_mul Nat.cast_mul Nat.not_even_two_mul_add_one
coeff_preΨ_ne_zero 📖	—	—	—	—	preΨ_ofNat coeff_preΨ'_ne_zero Nat.cast_zero Int.cast_zero Int.cast_natCast preΨ_neg Polynomial.coeff_neg neg_ne_zero
coeff_preΨ₄ 📖	mathematical	—	Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring preΨ₄ instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat preΨ₄.eq_1 Mathlib.Tactic.ComputeDegree.coeff_congr Mathlib.Tactic.ComputeDegree.coeff_add_of_eq Mathlib.Tactic.ComputeDegree.coeff_mul_add_of_le_natDegree_of_eq_ite Mathlib.Tactic.ComputeDegree.natDegree_natCast_le Polynomial.natDegree_pow_le_of_le Polynomial.natDegree_X_le Mathlib.Tactic.ComputeDegree.coeff_congr_lhs Polynomial.coeff_natCast_ite Mathlib.Tactic.ComputeDegree.coeff_pow_of_natDegree_le_of_eq_ite' Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat le_refl Polynomial.coeff_X Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.ComputeDegree.natDegree_C_le Polynomial.coeff_C Mathlib.Meta.NormNum.isNat_le_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Polynomial.natDegree_mul_le_of_le one_pow mul_one add_zero
coeff_preΨ₄_ne_zero 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat coeff_preΨ₄
coeff_Φ 📖	mathematical	—	Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring Φ Monoid.toNatPow Nat.instMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Φ_neg
coeff_Φ_ne_zero 📖	—	—	—	—	one_ne_zero NeZero.one coeff_Φ
coeff_ΨSq 📖	mathematical	—	Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring ΨSq Monoid.toNatPow Nat.instMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	Int.cast_natCast ΨSq_neg Int.cast_pow neg_sq
coeff_ΨSq_ne_zero 📖	—	—	—	—	coeff_ΨSq isReduced_of_noZeroDivisors Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
coeff_Ψ₂Sq 📖	mathematical	—	Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring Ψ₂Sq instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Ψ₂Sq.eq_1 Mathlib.Tactic.ComputeDegree.coeff_congr Mathlib.Tactic.ComputeDegree.coeff_add_of_eq Mathlib.Tactic.ComputeDegree.coeff_mul_add_of_le_natDegree_of_eq_ite Mathlib.Tactic.ComputeDegree.natDegree_C_le Polynomial.natDegree_pow_le_of_le Polynomial.natDegree_X_le Mathlib.Tactic.ComputeDegree.coeff_congr_lhs Polynomial.coeff_C Mathlib.Tactic.ComputeDegree.coeff_pow_of_natDegree_le_of_eq_ite' Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat le_refl Polynomial.coeff_X Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_le_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing one_pow mul_one add_zero
coeff_Ψ₂Sq_ne_zero 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat coeff_Ψ₂Sq
coeff_Ψ₃ 📖	mathematical	—	Polynomial.coeff CommSemiring.toSemiring CommRing.toCommSemiring Ψ₃ instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Ψ₃.eq_1 Mathlib.Tactic.ComputeDegree.coeff_congr Mathlib.Tactic.ComputeDegree.coeff_add_of_eq Mathlib.Tactic.ComputeDegree.coeff_mul_add_of_le_natDegree_of_eq_ite Mathlib.Tactic.ComputeDegree.natDegree_natCast_le Polynomial.natDegree_pow_le_of_le Polynomial.natDegree_X_le Mathlib.Tactic.ComputeDegree.coeff_congr_lhs Polynomial.coeff_natCast_ite Mathlib.Tactic.ComputeDegree.coeff_pow_of_natDegree_le_of_eq_ite' Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat le_refl Polynomial.coeff_X Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.ComputeDegree.natDegree_C_le Polynomial.coeff_C Mathlib.Meta.NormNum.isNat_le_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Polynomial.natDegree_mul_le_of_le one_pow mul_one add_zero
coeff_Ψ₃_ne_zero 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat coeff_Ψ₃
leadingCoeff_preΨ 📖	mathematical	—	Polynomial.leadingCoeff CommSemiring.toSemiring CommRing.toCommSemiring preΨ AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing Even Int.instDecidablePredEven	—	Polynomial.leadingCoeff.eq_1 natDegree_preΨ coeff_preΨ
leadingCoeff_preΨ' 📖	mathematical	—	Polynomial.leadingCoeff CommSemiring.toSemiring CommRing.toCommSemiring preΨ' AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Even Nat.instDecidablePredEven	—	Polynomial.leadingCoeff.eq_1 natDegree_preΨ' coeff_preΨ'
leadingCoeff_preΨ₄ 📖	mathematical	—	Polynomial.leadingCoeff CommSemiring.toSemiring CommRing.toCommSemiring preΨ₄ instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Polynomial.leadingCoeff.eq_1 natDegree_preΨ₄ coeff_preΨ₄
leadingCoeff_Φ 📖	mathematical	—	Polynomial.leadingCoeff CommSemiring.toSemiring CommRing.toCommSemiring Φ AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Polynomial.leadingCoeff.eq_1 natDegree_Φ coeff_Φ
leadingCoeff_ΨSq 📖	mathematical	—	Polynomial.leadingCoeff CommSemiring.toSemiring CommRing.toCommSemiring ΨSq Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	Polynomial.leadingCoeff.eq_1 natDegree_ΨSq coeff_ΨSq
leadingCoeff_Ψ₂Sq 📖	mathematical	—	Polynomial.leadingCoeff CommSemiring.toSemiring CommRing.toCommSemiring Ψ₂Sq instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Polynomial.leadingCoeff.eq_1 natDegree_Ψ₂Sq coeff_Ψ₂Sq
leadingCoeff_Ψ₃ 📖	mathematical	—	Polynomial.leadingCoeff CommSemiring.toSemiring CommRing.toCommSemiring Ψ₃ instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Polynomial.leadingCoeff.eq_1 natDegree_Ψ₃ coeff_Ψ₃
natDegree_preΨ 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring preΨ Monoid.toNatPow Nat.instMonoid Even Int.instDecidablePredEven	—	Polynomial.natDegree_eq_of_le_of_coeff_ne_zero natDegree_preΨ_le coeff_preΨ_ne_zero
natDegree_preΨ' 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring preΨ' Monoid.toNatPow Nat.instMonoid Even Nat.instDecidablePredEven	—	Polynomial.natDegree_eq_of_le_of_coeff_ne_zero natDegree_preΨ'_le coeff_preΨ'_ne_zero
natDegree_preΨ'_le 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring preΨ' Monoid.toNatPow Nat.instMonoid Even Nat.instDecidablePredEven	—	—
natDegree_preΨ'_pos 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring preΨ'	—	natDegree_preΨ' Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid LE.le.trans Nat.AtLeastTwo.prop Nat.instAtLeastTwoHAddOfNat
natDegree_preΨ_le 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring preΨ Monoid.toNatPow Nat.instMonoid Even Int.instDecidablePredEven	—	natDegree_preΨ'_le preΨ_ofNat preΨ_neg Polynomial.natDegree_neg
natDegree_preΨ_pos 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring preΨ	—	preΨ_ofNat natDegree_preΨ'_pos Nat.cast_zero Int.cast_zero Int.cast_natCast preΨ_neg Polynomial.natDegree_neg neg_ne_zero
natDegree_preΨ₄ 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring preΨ₄	—	Nat.instAtLeastTwoHAddOfNat Polynomial.natDegree_eq_of_le_of_coeff_ne_zero natDegree_preΨ₄_le coeff_preΨ₄_ne_zero
natDegree_preΨ₄_le 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring preΨ₄	—	preΨ₄.eq_1 le_trans Polynomial.natDegree_add_le_of_le Polynomial.natDegree_mul_le_of_le Mathlib.Tactic.ComputeDegree.natDegree_natCast_le Polynomial.natDegree_pow_le_of_le Polynomial.natDegree_X_le Mathlib.Tactic.ComputeDegree.natDegree_C_le Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_mul sup_of_le_left Mathlib.Meta.NormNum.isNat_le_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one Nat.cast_zero le_refl
natDegree_preΨ₄_pos 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring preΨ₄	—	Nat.instAtLeastTwoHAddOfNat lt_of_not_ge 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.atom_pf Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.sub_pf 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.IsInt.to_isNat Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Int.instCharZero Mathlib.Tactic.Linarith.sub_nonpos_of_le Nat.cast_zero neg_eq_zero sub_eq_zero_of_eq natDegree_preΨ₄
natDegree_Φ 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring Φ Monoid.toNatPow Nat.instMonoid	—	Polynomial.natDegree_eq_of_le_of_coeff_ne_zero natDegree_Φ_le coeff_Φ_ne_zero
natDegree_Φ_le 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring Φ Monoid.toNatPow Nat.instMonoid	—	Φ_neg
natDegree_Φ_pos 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring Φ	—	natDegree_Φ Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd
natDegree_ΨSq 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring ΨSq Monoid.toNatPow Nat.instMonoid	—	Polynomial.natDegree_eq_of_le_of_coeff_ne_zero natDegree_ΨSq_le coeff_ΨSq_ne_zero
natDegree_ΨSq_le 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring ΨSq Monoid.toNatPow Nat.instMonoid	—	ΨSq_neg
natDegree_ΨSq_pos 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring ΨSq	—	natDegree_ΨSq Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
natDegree_Ψ₂Sq 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring Ψ₂Sq	—	Nat.instAtLeastTwoHAddOfNat Polynomial.natDegree_eq_of_le_of_coeff_ne_zero natDegree_Ψ₂Sq_le coeff_Ψ₂Sq_ne_zero
natDegree_Ψ₂Sq_le 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring Ψ₂Sq	—	Ψ₂Sq.eq_1 le_trans Polynomial.natDegree_add_le_of_le Polynomial.natDegree_mul_le_of_le Mathlib.Tactic.ComputeDegree.natDegree_C_le Polynomial.natDegree_pow_le_of_le Polynomial.natDegree_X_le Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_mul sup_of_le_left Mathlib.Meta.NormNum.isNat_le_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one Nat.cast_zero le_refl
natDegree_Ψ₂Sq_pos 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring Ψ₂Sq	—	Nat.instAtLeastTwoHAddOfNat three_pos Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid natDegree_Ψ₂Sq
natDegree_Ψ₃ 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring Ψ₃	—	Nat.instAtLeastTwoHAddOfNat Polynomial.natDegree_eq_of_le_of_coeff_ne_zero natDegree_Ψ₃_le coeff_Ψ₃_ne_zero
natDegree_Ψ₃_le 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring Ψ₃	—	Ψ₃.eq_1 le_trans Polynomial.natDegree_add_le_of_le Polynomial.natDegree_mul_le_of_le Mathlib.Tactic.ComputeDegree.natDegree_natCast_le Polynomial.natDegree_pow_le_of_le Polynomial.natDegree_X_le Mathlib.Tactic.ComputeDegree.natDegree_C_le Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isNat_mul sup_of_le_left Mathlib.Meta.NormNum.isNat_le_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one Nat.cast_zero le_refl
natDegree_Ψ₃_pos 📖	mathematical	—	Polynomial.natDegree CommSemiring.toSemiring CommRing.toCommSemiring Ψ₃	—	Nat.instAtLeastTwoHAddOfNat four_pos Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid natDegree_Ψ₃
preΨ'_ne_zero 📖	—	—	—	—	Polynomial.ne_zero_of_natDegree_gt natDegree_preΨ'_pos Nat.cast_zero zero_add preΨ'_one NeZero.one Polynomial.nontrivial IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd preΨ'_two
preΨ_ne_zero 📖	—	—	—	—	preΨ_ofNat preΨ'_ne_zero Nat.cast_zero Int.cast_zero Int.cast_natCast preΨ_neg neg_ne_zero
preΨ₄_ne_zero 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat Polynomial.ne_zero_of_natDegree_gt natDegree_preΨ₄_pos
Φ_ne_zero 📖	—	—	—	—	Φ_zero one_ne_zero NeZero.one Polynomial.nontrivial Polynomial.ne_zero_of_natDegree_gt natDegree_Φ_pos
ΨSq_ne_zero 📖	—	—	—	—	Polynomial.ne_zero_of_natDegree_gt natDegree_ΨSq_pos Int.cast_zero Nat.cast_one ΨSq_one Polynomial.C_injective Int.cast_one Polynomial.C_0 ΨSq_neg Int.cast_neg Polynomial.C_neg neg_zero
Ψ₂Sq_ne_zero 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat Polynomial.ne_zero_of_natDegree_gt natDegree_Ψ₂Sq_pos
Ψ₃_ne_zero 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat Polynomial.ne_zero_of_natDegree_gt natDegree_Ψ₃_pos

---

← Back to Index