Commit 2024-06-24 11:40 dc3d440d

View on Github →

feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree): add further degree lemmas (#14063)

Estimated changes

Modified Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean

added theorem WeierstrassCurve.coeff_preΨ'_ne_zero

added theorem WeierstrassCurve.coeff_preΨ_ne_zero

added theorem WeierstrassCurve.coeff_preΨ₄_ne_zero

added theorem WeierstrassCurve.coeff_Φ_ne_zero

added theorem WeierstrassCurve.coeff_ΨSq_ne_zero

added theorem WeierstrassCurve.coeff_Ψ₂Sq_ne_zero

added theorem WeierstrassCurve.coeff_Ψ₃_ne_zero

added theorem WeierstrassCurve.leadingCoeff_preΨ'

added theorem WeierstrassCurve.leadingCoeff_preΨ

added theorem WeierstrassCurve.leadingCoeff_preΨ₄

added theorem WeierstrassCurve.leadingCoeff_Φ

added theorem WeierstrassCurve.leadingCoeff_ΨSq

added theorem WeierstrassCurve.leadingCoeff_Ψ₂Sq

added theorem WeierstrassCurve.leadingCoeff_Ψ₃

modified theorem WeierstrassCurve.natDegree_preΨ'

added theorem WeierstrassCurve.natDegree_preΨ'_le

added theorem WeierstrassCurve.natDegree_preΨ'_pos

modified theorem WeierstrassCurve.natDegree_preΨ

added theorem WeierstrassCurve.natDegree_preΨ_le

added theorem WeierstrassCurve.natDegree_preΨ_pos

modified theorem WeierstrassCurve.natDegree_preΨ₄

added theorem WeierstrassCurve.natDegree_preΨ₄_le

added theorem WeierstrassCurve.natDegree_preΨ₄_pos

modified theorem WeierstrassCurve.natDegree_Φ

added theorem WeierstrassCurve.natDegree_Φ_le

added theorem WeierstrassCurve.natDegree_Φ_pos

modified theorem WeierstrassCurve.natDegree_ΨSq

added theorem WeierstrassCurve.natDegree_ΨSq_le

added theorem WeierstrassCurve.natDegree_ΨSq_pos

modified theorem WeierstrassCurve.natDegree_Ψ₂Sq

added theorem WeierstrassCurve.natDegree_Ψ₂Sq_le

added theorem WeierstrassCurve.natDegree_Ψ₂Sq_pos

modified theorem WeierstrassCurve.natDegree_Ψ₃

added theorem WeierstrassCurve.natDegree_Ψ₃_le

added theorem WeierstrassCurve.natDegree_Ψ₃_pos

added theorem WeierstrassCurve.preΨ'_ne_zero

added theorem WeierstrassCurve.preΨ_ne_zero

added theorem WeierstrassCurve.preΨ₄_ne_zero

added theorem WeierstrassCurve.Φ_ne_zero

added theorem WeierstrassCurve.ΨSq_ne_zero

added theorem WeierstrassCurve.Ψ₂Sq_ne_zero

added theorem WeierstrassCurve.Ψ₃_ne_zero