Point

📁 Source: Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

Statistics

Metric	Count
Definitions CoordinateRing, XClass, XIdeal, XYIdeal, XYIdeal', YClass, YIdeal, basis, instAlgebra, instAlgebraPolynomial, map, mk, quotientXYIdealEquiv, Point, add, baseChange, instAdd, instAddCommGroup, instAddCommSemigroup, instAddZeroClass, instInhabited, instInvolutiveNeg, instNeg, instZero, map, neg, toClass, «term_⟮_⟯»	28
Theorems C_addPolynomial, C_addPolynomial_slope, XClass_ne_zero, XYIdeal'_eq, XYIdeal_add_eq, XYIdeal_eq₁, XYIdeal_eq₂, XYIdeal_mul_XYIdeal, XYIdeal_neg_mul, YClass_ne_zero, basis_apply, basis_one, basis_zero, coe_basis, coe_norm_smul_basis, degree_norm_ne_one, degree_norm_smul_basis, exists_smul_basis_eq, instIsDomain, instIsScalarTowerPolynomial, instSubsingleton, map_injective, map_mk, map_smul, mk_XYIdeal'_mul_mk_XYIdeal', mk_XYIdeal'_neg_mul, natDegree_norm_ne_one, norm_smul_basis, smul, smul_basis_eq_zero, smul_basis_mul_C, smul_basis_mul_Y, add_def, add_of_X_ne, add_of_X_ne', add_of_Y_eq, add_of_Y_ne, add_of_Y_ne', add_self_of_Y_eq, add_self_of_Y_ne, add_self_of_Y_ne', add_some, map_baseChange, map_id, map_injective, map_map, map_some, map_zero, neg_def, neg_some, neg_zero, some_ne_zero, toClass_apply, toClass_eq_zero, toClass_injective, toClass_some, toClass_zero, zero_def	58
Total	86

WeierstrassCurve.Affine

Definitions

Name	Category	Theorems
CoordinateRing 📖	CompOp	34 math math: CoordinateRing.smul, CoordinateRing.basis_one, CoordinateRing.smul_basis_mul_C, CoordinateRing.coe_basis, Point.toClass_zero, CoordinateRing.instIsScalarTowerPolynomial, CoordinateRing.mk_ψ, CoordinateRing.C_addPolynomial, CoordinateRing.mk_XYIdeal'_neg_mul, CoordinateRing.XYIdeal_add_eq, CoordinateRing.norm_smul_basis, CoordinateRing.degree_norm_smul_basis, CoordinateRing.instSubsingleton, CoordinateRing.map_mk, CoordinateRing.mk_φ, CoordinateRing.instIsDomain, CoordinateRing.mk_Ψ_sq, CoordinateRing.XYIdeal_neg_mul, CoordinateRing.exists_smul_basis_eq, CoordinateRing.C_addPolynomial_slope, CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', CoordinateRing.map_injective, Point.toClass_some, Point.toClass_injective, CoordinateRing.coe_norm_smul_basis, CoordinateRing.mk_ψ₂_sq, CoordinateRing.basis_zero, Point.toClass_eq_zero, CoordinateRing.XYIdeal'_eq, CoordinateRing.map_smul, CoordinateRing.basis_apply, Point.toClass_apply, CoordinateRing.smul_basis_mul_Y, CoordinateRing.XYIdeal_mul_XYIdeal
Point 📖	CompData	49 math math: WeierstrassCurve.Jacobian.Point.toAffineLift_neg, WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero, Point.add_self_of_Y_ne, Point.toClass_zero, WeierstrassCurve.Projective.Point.toAffineAddEquiv_apply, WeierstrassCurve.Projective.Point.toAffineLift_neg, WeierstrassCurve.Projective.Point.toAffineLift_zero, WeierstrassCurve.Jacobian.Point.toAffine_neg, Point.add_of_X_ne, WeierstrassCurve.Projective.Point.toAffineLift_of_Z_eq_zero, Point.neg_def, Point.map_injective, Point.add_self_of_Y_ne', WeierstrassCurve.Projective.Point.toAffine_of_singular, Point.neg_some, WeierstrassCurve.Jacobian.Point.toAffineLift_add, Point.zero_def, Point.add_def, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_apply, Point.map_baseChange, WeierstrassCurve.Projective.Point.toAffine_neg, Point.add_of_Y_ne, WeierstrassCurve.Jacobian.Point.toAffine_add, Point.add_of_Y_eq, Point.map_map, Point.neg_zero, Point.toClass_some, Point.toClass_injective, Point.add_some, WeierstrassCurve.Projective.Point.toAffineLift_add, Point.add_self_of_Y_eq, Point.map_some, WeierstrassCurve.Projective.Point.toAffine_add, WeierstrassCurve.Jacobian.Point.toAffineLift_zero, WeierstrassCurve.Jacobian.Point.toAffine_zero, Point.add_of_Y_ne', Point.add_of_X_ne', WeierstrassCurve.Projective.Point.toAffine_of_Z_eq_zero, Point.toClass_eq_zero, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_symm_apply, WeierstrassCurve.Projective.Point.toAffine_zero, WeierstrassCurve.Projective.Point.fromAffine_zero, WeierstrassCurve.Projective.Point.toAffineAddEquiv_symm_apply, Point.map_zero, WeierstrassCurve.Jacobian.Point.toAffine_of_singular, WeierstrassCurve.Jacobian.Point.toAffineLift_of_Z_eq_zero, Point.toClass_apply, Point.map_id, WeierstrassCurve.Jacobian.Point.fromAffine_zero
«term_⟮_⟯» 📖	CompOp	—

WeierstrassCurve.Affine.CoordinateRing

Definitions

Name	Category	Theorems
XClass 📖	CompOp	1 math math: C_addPolynomial_slope
XIdeal 📖	CompOp	3 math math: XYIdeal_add_eq, XYIdeal_neg_mul, XYIdeal_mul_XYIdeal
XYIdeal 📖	CompOp	6 math math: XYIdeal_eq₂, XYIdeal_add_eq, XYIdeal_neg_mul, XYIdeal_eq₁, XYIdeal'_eq, XYIdeal_mul_XYIdeal
XYIdeal' 📖	CompOp	5 math math: mk_XYIdeal'_neg_mul, mk_XYIdeal'_mul_mk_XYIdeal', WeierstrassCurve.Affine.Point.toClass_some, XYIdeal'_eq, WeierstrassCurve.Affine.Point.toClass_apply
YClass 📖	CompOp	—
YIdeal 📖	CompOp	1 math math: XYIdeal_mul_XYIdeal
basis 📖	CompOp	4 math math: basis_one, coe_basis, basis_zero, basis_apply
instAlgebra 📖	CompOp	—
instAlgebraPolynomial 📖	CompOp	7 math math: basis_one, coe_basis, norm_smul_basis, degree_norm_smul_basis, coe_norm_smul_basis, basis_zero, basis_apply
map 📖	CompOp	3 math math: map_mk, map_injective, map_smul
mk 📖	CompOp	—
quotientXYIdealEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_addPolynomial 📖	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 Polynomial.C WeierstrassCurve.Affine.addPolynomial Polynomial.instMul Polynomial.instSub Polynomial.ring CommRing.toRing Polynomial.X WeierstrassCurve.Affine.linePolynomial WeierstrassCurve.Affine.negPolynomial	—	WeierstrassCurve.Affine.C_addPolynomial add_sub_cancel_left mul_one
C_addPolynomial_slope 📖	mathematical	WeierstrassCurve.Affine.Equation EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Affine.negY	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring WeierstrassCurve.Affine.CoordinateRing Semiring.toNonAssocSemiring AdjoinRoot.instCommRing Polynomial.commRing WeierstrassCurve.Affine.polynomial RingHom.instFunLike Polynomial.C WeierstrassCurve.Affine.addPolynomial WeierstrassCurve.Affine.slope NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing XClass WeierstrassCurve.Affine.addX	—	WeierstrassCurve.Affine.C_addPolynomial_slope
XClass_ne_zero 📖	—	—	—	—	AdjoinRoot.mk_ne_zero_of_natDegree_lt WeierstrassCurve.Affine.monic_polynomial Polynomial.C_ne_zero Polynomial.X_sub_C_ne_zero WeierstrassCurve.Affine.natDegree_polynomial Polynomial.natDegree_C Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instCharZero Mathlib.Meta.NormNum.isNat_ofNat
XYIdeal'_eq 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	Units.val FractionalIdeal WeierstrassCurve.Affine.CoordinateRing AdjoinRoot.instCommRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing WeierstrassCurve.Affine.polynomial nonZeroDivisors Semiring.toMonoidWithZero WeierstrassCurve.Affine.FunctionField OreLocalization.instCommRing OreLocalization.oreSetComm CommRing.toCommMonoid OreLocalization.instAlgebra Algebra.id MonoidWithZero.toMonoid FractionalIdeal.commSemiring XYIdeal' FractionalIdeal.coeIdeal XYIdeal DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C	—	—
XYIdeal_add_eq 📖	mathematical	—	XYIdeal WeierstrassCurve.Affine.addX DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C WeierstrassCurve.Affine.addY Ideal WeierstrassCurve.Affine.CoordinateRing AdjoinRoot.instCommRing Polynomial.commRing WeierstrassCurve.Affine.polynomial SemilatticeSup.toMax IdemSemiring.toSemilatticeSup Submodule.idemSemiring Algebra.id Ideal.span Set Set.instSingletonSet Polynomial.instSub Polynomial.ring CommRing.toRing WeierstrassCurve.Affine.negPolynomial WeierstrassCurve.Affine.linePolynomial XIdeal	—	sub_sub neg_sub_left map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Ideal.span_singleton_neg sup_comm Ideal.span_insert Ideal.span_pair_add_mul_right map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_add AddMonoidHomClass.toAddHomClass Polynomial.C_sub Polynomial.C_neg Polynomial.C_add Polynomial.C_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr 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.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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add
XYIdeal_eq₁ 📖	mathematical	—	XYIdeal DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C WeierstrassCurve.Affine.linePolynomial	—	Ideal.span_pair_add_mul_right map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass Polynomial.C_sub Polynomial.C_neg Polynomial.C_add Polynomial.C_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_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.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_congr Mathlib.Tactic.Ring.neg_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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt
XYIdeal_eq₂ 📖	mathematical	WeierstrassCurve.Affine.Equation EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Affine.negY	XYIdeal DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C WeierstrassCurve.Affine.linePolynomial WeierstrassCurve.Affine.slope	—	Polynomial.eval_add Polynomial.eval_mul Polynomial.eval_C Polynomial.eval_sub Polynomial.eval_X sub_self MulZeroClass.mul_zero zero_add WeierstrassCurve.Affine.Y_eq_of_Y_ne WeierstrassCurve.Affine.slope_of_X_ne Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg sub_ne_zero_of_ne Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.subst_sub Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_congr 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.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.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Ideal.span_pair_add_mul_right map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass Polynomial.C_add Polynomial.C_mul Polynomial.C_sub Polynomial.C_neg Mathlib.Tactic.Ring.neg_congr
XYIdeal_mul_XYIdeal 📖	mathematical	WeierstrassCurve.Affine.Equation EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Affine.negY	Ideal WeierstrassCurve.Affine.CoordinateRing CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot.instCommRing Polynomial Polynomial.commRing WeierstrassCurve.Affine.polynomial Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id XIdeal WeierstrassCurve.Affine.addX WeierstrassCurve.Affine.slope XYIdeal DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C YIdeal WeierstrassCurve.Affine.linePolynomial WeierstrassCurve.Affine.addY	—	sup_assoc sup_comm sup_sup_sup_comm IsScalarTower.right XYIdeal_add_eq XIdeal.eq_1 mul_comm XYIdeal_eq₁ XYIdeal.eq_1 XYIdeal_eq₂ IsScalarTower.left Ideal.span_pair_mul_span_pair Ideal.instIsTwoSided_1 Ideal.span_insert Ideal.sup_mul Ideal.span_singleton_mul_span_singleton neg_eq_iff_eq_neg C_addPolynomial_slope Ideal.span_singleton_neg C_addPolynomial map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass YClass.eq_1 mul_assoc Ideal.span_pair_add_mul_right mul_neg sub_eq_add_neg sub_mul map_sub RingHomClass.toAddMonoidHomClass sub_sub_sub_cancel_right Set.image_singleton Ideal.mem_map_iff_of_surjective AdjoinRoot.mk_surjective pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain sub_ne_zero_of_ne Nat.instAtLeastTwoHAddOfNat WeierstrassCurve.Affine.polynomial.eq_1 WeierstrassCurve.Affine.negPolynomial.eq_1 mul_right_inj' Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Polynomial.C_ne_zero mul_inv_cancel₀ mul_add Distrib.leftDistribClass Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq WeierstrassCurve.Affine.equation_iff Mathlib.Tactic.LinearCombination.eq_rearrange WeierstrassCurve.b₂.eq_1 WeierstrassCurve.b₄.eq_1 WeierstrassCurve.Affine.negY.eq_1 Polynomial.C_add Polynomial.C_mul Polynomial.C_pow Polynomial.C_sub Polynomial.C_neg map_ofNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_congr 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_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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.pow_congr 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.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.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero map_add AddMonoidHomClass.toAddHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AdjoinRoot.mk_self MulZeroClass.mul_zero add_zero WeierstrassCurve.Affine.Y_eq_of_Y_ne Ideal.top_mul
XYIdeal_neg_mul 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	Ideal WeierstrassCurve.Affine.CoordinateRing CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot.instCommRing Polynomial Polynomial.commRing WeierstrassCurve.Affine.polynomial Submodule.mul Semiring.toModule IsScalarTower.right Algebra.id XYIdeal DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C WeierstrassCurve.Affine.negY XIdeal	—	Mathlib.Tactic.LinearCombination.eq_of_eq AddRightCancelSemigroup.toIsRightCancelAdd WeierstrassCurve.Affine.equation_iff Mathlib.Tactic.LinearCombination.eq_rearrange WeierstrassCurve.Affine.negY.eq_1 WeierstrassCurve.Affine.polynomial.eq_1 Polynomial.C_sub Polynomial.C_neg Polynomial.C_mul Polynomial.C_add Polynomial.C_pow Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_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.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.neg_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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add 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_pow Mathlib.Tactic.Ring.pow_zero Nat.cast_one Mathlib.Tactic.Ring.cast_zero Nat.cast_zero IsScalarTower.right Ideal.span_pair_mul_span_pair Ideal.instIsTwoSided_1 mul_comm NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_mul Ideal.span_insert IsScalarTower.left Set.image_singleton Nat.instAtLeastTwoHAddOfNat WeierstrassCurve.Affine.nonsingular_iff' mul_right_inj' Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain Polynomial.C_ne_zero mul_inv_cancel₀ mul_add Distrib.leftDistribClass map_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Ideal.map_top Ideal.mul_top
YClass_ne_zero 📖	—	—	—	—	AdjoinRoot.mk_ne_zero_of_natDegree_lt WeierstrassCurve.Affine.monic_polynomial Polynomial.X_sub_C_ne_zero Polynomial.nontrivial WeierstrassCurve.Affine.natDegree_polynomial Polynomial.natDegree_X_sub_C Mathlib.Meta.NormNum.isNat_lt_true IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instCharZero Mathlib.Meta.NormNum.isNat_ofNat
basis_apply 📖	mathematical	—	DFunLike.coe Module.Basis Polynomial CommSemiring.toSemiring CommRing.toCommSemiring WeierstrassCurve.Affine.CoordinateRing Polynomial.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AdjoinRoot.instCommRing Polynomial.commRing WeierstrassCurve.Affine.polynomial Algebra.toModule Polynomial.commSemiring instAlgebraPolynomial Module.Basis.instFunLike basis AdjoinRoot Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero PowerBasis.gen CommRing.toRing AdjoinRoot.instAlgebra Algebra.id AdjoinRoot.powerBasis' WeierstrassCurve.Affine.monic_polynomial	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim WeierstrassCurve.Affine.monic_polynomial instSubsingleton subsingleton_or_nontrivial WeierstrassCurve.Affine.natDegree_polynomial basis.eq_1 Or.by_cases.eq_1 not_subsingleton Module.Basis.reindex_apply PowerBasis.basis_eq_pow finCongr_symm_apply
basis_one 📖	mathematical	—	DFunLike.coe Module.Basis Polynomial CommSemiring.toSemiring CommRing.toCommSemiring WeierstrassCurve.Affine.CoordinateRing Polynomial.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AdjoinRoot.instCommRing Polynomial.commRing WeierstrassCurve.Affine.polynomial Algebra.toModule Polynomial.commSemiring instAlgebraPolynomial Module.Basis.instFunLike basis RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.X	—	WeierstrassCurve.Affine.monic_polynomial basis_apply pow_one
basis_zero 📖	mathematical	—	DFunLike.coe Module.Basis Polynomial CommSemiring.toSemiring CommRing.toCommSemiring WeierstrassCurve.Affine.CoordinateRing Polynomial.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AdjoinRoot.instCommRing Polynomial.commRing WeierstrassCurve.Affine.polynomial Algebra.toModule Polynomial.commSemiring instAlgebraPolynomial Module.Basis.instFunLike basis AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	WeierstrassCurve.Affine.monic_polynomial basis_apply pow_zero
coe_basis 📖	mathematical	—	DFunLike.coe Module.Basis Polynomial CommSemiring.toSemiring CommRing.toCommSemiring WeierstrassCurve.Affine.CoordinateRing Polynomial.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AdjoinRoot.instCommRing Polynomial.commRing WeierstrassCurve.Affine.polynomial Algebra.toModule Polynomial.commSemiring instAlgebraPolynomial Module.Basis.instFunLike basis Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.X Matrix.vecEmpty	—	Fintype.complete basis_zero basis_one
coe_norm_smul_basis 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Polynomial.commRing WeierstrassCurve.Affine.polynomial Semiring.toNonAssocSemiring AdjoinRoot.instCommRing RingHom.instFunLike AdjoinRoot.of MonoidHom WeierstrassCurve.Affine.CoordinateRing MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring CommRing.toRing MonoidHom.instFunLike Algebra.norm instAlgebraPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AdjoinRoot.instSMulAdjoinRoot NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right Polynomial.commSemiring Algebra.id AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Polynomial.semiring Polynomial.X Polynomial.instMul Polynomial.instAdd Polynomial.C Polynomial.instSub Polynomial.ring Polynomial.instNeg WeierstrassCurve.a₁ WeierstrassCurve.a₃	—	IsScalarTower.right norm_smul_basis Polynomial.C_sub Polynomial.C_pow Polynomial.C_mul Polynomial.C_add Mathlib.Tactic.Ring.of_eq 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_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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_gt Mathlib.Tactic.Ring.neg_congr 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.mul_one
degree_norm_ne_one 📖	—	—	—	—	IsScalarTower.right exists_smul_basis_eq Nat.instAtLeastTwoHAddOfNat degree_norm_smul_basis LT.lt.ne' lt_max_of_lt_right cmp_eq_lt_iff
degree_norm_smul_basis 📖	mathematical	—	Polynomial.degree CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidHom WeierstrassCurve.Affine.CoordinateRing Polynomial MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing AdjoinRoot.instCommRing Polynomial.commRing WeierstrassCurve.Affine.polynomial MonoidHom.instFunLike Algebra.norm instAlgebraPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AdjoinRoot.instSMulAdjoinRoot NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right Polynomial.commSemiring Algebra.id AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne RingHom Polynomial.semiring RingHom.instFunLike Polynomial.X WithBot SemilatticeSup.toMax WithBot.semilatticeSup Lattice.toSemilatticeSup Nat.instLattice AddMonoid.toNatSMul WithBot.addMonoid Nat.instAddMonoid WithBot.add instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	—	Polynomial.degree_pow IsDomain.to_noZeroDivisors IsDomain.toNontrivial Polynomial.degree_mul le_imp_le_of_le_of_le add_le_add_right WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Polynomial.degree_linear_le le_refl Nat.instAtLeastTwoHAddOfNat one_mul Polynomial.C_1 Polynomial.degree_cubic one_ne_zero' NeZero.one IsScalarTower.right norm_smul_basis zero_pow two_ne_zero MulZeroClass.zero_mul zero_sub neg_zero Polynomial.degree_neg max_bot_left MulZeroClass.mul_zero sub_zero max_bot_right Polynomial.degree_eq_bot le_or_gt Polynomial.degree_sub_eq_right_of_degree_lt LE.le.trans_lt Polynomial.degree_sub_le max_lt_iff Eq.trans_lt WithBot.coe_lt_coe lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing Nat.cast_add Nat.cast_mul Mathlib.Tactic.Linarith.mul_nonpos Nat.cast_one Mathlib.Meta.NormNum.isNat_lt_true Int.instCharZero Mathlib.Tactic.Ring.add_overlap_pf max_eq_right_of_lt sub_sub Polynomial.degree_sub_eq_left_of_degree_lt Polynomial.degree_add_le Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_mul max_eq_left_of_lt
exists_smul_basis_eq 📖	mathematical	—	WeierstrassCurve.Affine.CoordinateRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AdjoinRoot.instCommRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing WeierstrassCurve.Affine.polynomial AdjoinRoot.instSMulAdjoinRoot NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right Polynomial.commSemiring Algebra.id AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe RingHom Polynomial.semiring Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.X	—	RingHomInvPair.ids Finite.of_fintype Module.Basis.sum_equivFun IsScalarTower.right basis_one basis_zero Fin.sum_univ_one Fin.sum_univ_succ
instIsDomain 📖	mathematical	—	IsDomain WeierstrassCurve.Affine.CoordinateRing CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot.instCommRing Polynomial Polynomial.commRing WeierstrassCurve.Affine.polynomial	—	AdjoinRoot.isDomain_of_prime Irreducible.prime UniqueFactorizationMonoid.instDecompositionMonoid Polynomial.uniqueFactorizationMonoid PrincipalIdealRing.to_uniqueFactorizationMonoid instIsDomain EuclideanDomain.to_principal_ideal_domain WeierstrassCurve.Affine.irreducible_polynomial Function.Injective.isDomain RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_injective IsFractionRing.injective Localization.isLocalization
instIsScalarTowerPolynomial 📖	mathematical	—	IsScalarTower Polynomial CommSemiring.toSemiring CommRing.toCommSemiring WeierstrassCurve.Affine.CoordinateRing Algebra.toSMul Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AdjoinRoot.instSMulAdjoinRoot Polynomial.commRing WeierstrassCurve.Affine.polynomial NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsScalarTower.right Polynomial.commSemiring Polynomial.distribSMul	—	Ideal.Quotient.isScalarTower Polynomial.isScalarTower IsScalarTower.right
instSubsingleton 📖	mathematical	—	WeierstrassCurve.Affine.CoordinateRing	—	Module.subsingleton Unique.instSubsingleton
map_injective 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	WeierstrassCurve.Affine.CoordinateRing WeierstrassCurve.toAffine WeierstrassCurve.map AdjoinRoot.instCommRing Polynomial Polynomial.commRing WeierstrassCurve.Affine.polynomial map	—	injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass IsScalarTower.right exists_smul_basis_eq smul_basis_eq_zero Polynomial.map_X map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_smul map_add AddMonoidHomClass.toAddHomClass Polynomial.map_eq_zero_iff zero_smul add_zero
map_mk 📖	mathematical	—	DFunLike.coe RingHom WeierstrassCurve.Affine.CoordinateRing WeierstrassCurve.toAffine WeierstrassCurve.map Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot.instCommRing Polynomial Polynomial.commRing WeierstrassCurve.Affine.polynomial RingHom.instFunLike map Polynomial.semiring Polynomial.map Polynomial.mapRingHom	—	map.eq_1 Polynomial.eval₂_map AdjoinRoot.aeval_eq
map_smul 📖	mathematical	—	DFunLike.coe RingHom WeierstrassCurve.Affine.CoordinateRing WeierstrassCurve.toAffine WeierstrassCurve.map Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot.instCommRing Polynomial Polynomial.commRing WeierstrassCurve.Affine.polynomial RingHom.instFunLike map AdjoinRoot.instSMulAdjoinRoot NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsScalarTower.right Polynomial.commSemiring Algebra.id Polynomial.map	—	IsScalarTower.right smul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Polynomial.map_C
mk_XYIdeal'_mul_mk_XYIdeal' 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Affine.negY	ClassGroup WeierstrassCurve.Affine.CoordinateRing AdjoinRoot.instCommRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing WeierstrassCurve.Affine.polynomial instIsDomain instIsDomain Field.toSemifield MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup DFunLike.coe MonoidHom Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero WeierstrassCurve.Affine.FunctionField FractionRing.field OreLocalization.instAlgebra OreLocalization.oreSetComm CommRing.toCommMonoid Algebra.id MonoidWithZero.toMonoid FractionalIdeal.commSemiring Units.instMulOneClass MonoidHom.instFunLike Localization.isLocalization XYIdeal' WeierstrassCurve.Affine.addX WeierstrassCurve.Affine.slope WeierstrassCurve.Affine.addY WeierstrassCurve.Affine.nonsingular_add	—	instIsDomain instIsDomain Localization.isLocalization WeierstrassCurve.Affine.nonsingular_add map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass IsScalarTower.right ClassGroup.mk_eq_mk_of_coe_ideal FractionalIdeal.coeIdeal_mul XYIdeal'_eq XClass_ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing YClass_ne_zero XYIdeal_mul_XYIdeal
mk_XYIdeal'_neg_mul 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	ClassGroup WeierstrassCurve.Affine.CoordinateRing AdjoinRoot.instCommRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing WeierstrassCurve.Affine.polynomial instIsDomain instIsDomain Field.toSemifield MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup DFunLike.coe MonoidHom Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero WeierstrassCurve.Affine.FunctionField FractionRing.field OreLocalization.instAlgebra OreLocalization.oreSetComm CommRing.toCommMonoid Algebra.id MonoidWithZero.toMonoid FractionalIdeal.commSemiring Units.instMulOneClass MonoidHom.instFunLike Localization.isLocalization XYIdeal' WeierstrassCurve.Affine.negY WeierstrassCurve.Affine.nonsingular_neg InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	instIsDomain instIsDomain Localization.isLocalization WeierstrassCurve.Affine.nonsingular_neg map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass ClassGroup.mk_eq_one_of_coe_ideal IsScalarTower.right FractionalIdeal.coeIdeal_mul XYIdeal_neg_mul XClass_ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing
natDegree_norm_ne_one 📖	—	—	—	—	degree_norm_ne_one Polynomial.degree_eq_iff_natDegree_eq_of_pos zero_lt_one Nat.instZeroLEOneClass
norm_smul_basis 📖	mathematical	—	DFunLike.coe MonoidHom WeierstrassCurve.Affine.CoordinateRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring CommRing.toRing AdjoinRoot.instCommRing Polynomial.commRing WeierstrassCurve.Affine.polynomial MonoidHom.instFunLike Algebra.norm instAlgebraPolynomial Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AdjoinRoot.instSMulAdjoinRoot NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right Polynomial.commSemiring Algebra.id AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne RingHom Polynomial.semiring RingHom.instFunLike Polynomial.X Polynomial.instSub Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.instMul Polynomial.instAdd Polynomial.C WeierstrassCurve.a₁ WeierstrassCurve.a₃ WeierstrassCurve.a₂ WeierstrassCurve.a₄ WeierstrassCurve.a₆	—	IsScalarTower.right Algebra.norm_eq_matrix_det Matrix.det_fin_two RingHomInvPair.ids Algebra.leftMulMatrix_eq_repr_mul basis_zero mul_one basis_one smul_basis_mul_Y map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass map_smul SemilinearMapClass.toMulActionSemiHomClass Module.Basis.repr_self_apply Fin.instNeZeroHAddNatOfNat_mathlib_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_congr 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_pf_right Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt 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.mul_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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
smul 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring WeierstrassCurve.Affine.CoordinateRing AdjoinRoot.instSMulAdjoinRoot Polynomial.commRing WeierstrassCurve.Affine.polynomial NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsScalarTower.right Polynomial.commSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AdjoinRoot.instCommRing DFunLike.coe RingHom Polynomial.semiring Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	—	algebraMap_smul IsScalarTower.right
smul_basis_eq_zero 📖	mathematical	WeierstrassCurve.Affine.CoordinateRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AdjoinRoot.instCommRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing WeierstrassCurve.Affine.polynomial AdjoinRoot.instSMulAdjoinRoot NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right Polynomial.commSemiring Algebra.id AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe RingHom Polynomial.semiring Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.X MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Polynomial.instZero	—	IsScalarTower.right Fintype.linearIndependent_iff Module.Basis.linearIndependent basis_one Fin.sum_univ_one basis_zero Fin.sum_univ_succ
smul_basis_mul_C 📖	mathematical	—	WeierstrassCurve.Affine.CoordinateRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AdjoinRoot.instCommRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing WeierstrassCurve.Affine.polynomial Distrib.toAdd AdjoinRoot.instSMulAdjoinRoot NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right Polynomial.commSemiring Algebra.id AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe RingHom Polynomial.semiring Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.X Polynomial.C Polynomial.instMul	—	IsScalarTower.right smul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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_right Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add
smul_basis_mul_Y 📖	mathematical	—	WeierstrassCurve.Affine.CoordinateRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AdjoinRoot.instCommRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing WeierstrassCurve.Affine.polynomial Distrib.toAdd AdjoinRoot.instSMulAdjoinRoot NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.right Polynomial.commSemiring Algebra.id AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe RingHom Polynomial.semiring Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.X Polynomial.instMul Polynomial.instAdd Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.C WeierstrassCurve.a₂ WeierstrassCurve.a₄ WeierstrassCurve.a₆ Polynomial.instSub WeierstrassCurve.a₁ WeierstrassCurve.a₃	—	WeierstrassCurve.Affine.polynomial.eq_1 Mathlib.Tactic.Ring.of_eq 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_congr 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_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_congr Nat.cast_one Mathlib.Tactic.Ring.mul_one IsScalarTower.right smul add_mul Distrib.rightDistribClass mul_assoc map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass

WeierstrassCurve.Affine.Point

Definitions

Name	Category	Theorems
add 📖	CompOp	1 math math: add_def
baseChange 📖	CompOp	1 math math: map_baseChange
instAdd 📖	CompOp	18 math math: add_self_of_Y_ne, WeierstrassCurve.Projective.Point.toAffineAddEquiv_apply, add_of_X_ne, add_self_of_Y_ne', WeierstrassCurve.Jacobian.Point.toAffineLift_add, add_def, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_apply, add_of_Y_ne, WeierstrassCurve.Jacobian.Point.toAffine_add, add_of_Y_eq, add_some, WeierstrassCurve.Projective.Point.toAffineLift_add, add_self_of_Y_eq, WeierstrassCurve.Projective.Point.toAffine_add, add_of_Y_ne', add_of_X_ne', WeierstrassCurve.Jacobian.Point.toAffineAddEquiv_symm_apply, WeierstrassCurve.Projective.Point.toAffineAddEquiv_symm_apply
instAddCommGroup 📖	CompOp	—
instAddCommSemigroup 📖	CompOp	—
instAddZeroClass 📖	CompOp	11 math math: toClass_zero, map_injective, map_baseChange, map_map, toClass_some, toClass_injective, map_some, toClass_eq_zero, map_zero, toClass_apply, map_id
instInhabited 📖	CompOp	—
instInvolutiveNeg 📖	CompOp	—
instNeg 📖	CompOp	10 math math: WeierstrassCurve.Jacobian.Point.toAffineLift_neg, WeierstrassCurve.Projective.Point.toAffineLift_neg, WeierstrassCurve.Jacobian.Point.toAffine_neg, neg_def, add_self_of_Y_ne', neg_some, WeierstrassCurve.Projective.Point.toAffine_neg, neg_zero, add_of_Y_ne', add_of_X_ne'
instZero 📖	CompOp	19 math math: WeierstrassCurve.Jacobian.Point.toAffine_of_Z_eq_zero, toClass_zero, WeierstrassCurve.Projective.Point.toAffineLift_zero, WeierstrassCurve.Projective.Point.toAffineLift_of_Z_eq_zero, WeierstrassCurve.Projective.Point.toAffine_of_singular, zero_def, add_of_Y_eq, neg_zero, add_self_of_Y_eq, WeierstrassCurve.Jacobian.Point.toAffineLift_zero, WeierstrassCurve.Jacobian.Point.toAffine_zero, WeierstrassCurve.Projective.Point.toAffine_of_Z_eq_zero, toClass_eq_zero, WeierstrassCurve.Projective.Point.toAffine_zero, WeierstrassCurve.Projective.Point.fromAffine_zero, map_zero, WeierstrassCurve.Jacobian.Point.toAffine_of_singular, WeierstrassCurve.Jacobian.Point.toAffineLift_of_Z_eq_zero, WeierstrassCurve.Jacobian.Point.fromAffine_zero
map 📖	CompOp	6 math math: map_injective, map_baseChange, map_map, map_some, map_zero, map_id
neg 📖	CompOp	1 math math: neg_def
toClass 📖	CompOp	5 math math: toClass_zero, toClass_some, toClass_injective, toClass_eq_zero, toClass_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_def 📖	mathematical	—	WeierstrassCurve.Affine.Point EuclideanDomain.toCommRing Field.toEuclideanDomain instAdd add	—	—
add_of_X_ne 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	WeierstrassCurve.Affine.Point instAdd some WeierstrassCurve.Affine.addX WeierstrassCurve.Affine.slope WeierstrassCurve.Affine.addY WeierstrassCurve.Affine.nonsingular_add WeierstrassCurve.Affine.negY	—	add_some
add_of_X_ne' 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	WeierstrassCurve.Affine.Point instAdd some instNeg WeierstrassCurve.Affine.addX WeierstrassCurve.Affine.slope WeierstrassCurve.Affine.negAddY WeierstrassCurve.Affine.nonsingular_negAdd WeierstrassCurve.Affine.negY	—	add_of_X_ne
add_of_Y_eq 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Affine.negY	WeierstrassCurve.Affine.Point instAdd some instZero	—	WeierstrassCurve.Affine.nonsingular_add
add_of_Y_ne 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	WeierstrassCurve.Affine.Point instAdd some WeierstrassCurve.Affine.addX WeierstrassCurve.Affine.slope WeierstrassCurve.Affine.addY WeierstrassCurve.Affine.nonsingular_add WeierstrassCurve.Affine.negY	—	add_some
add_of_Y_ne' 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	WeierstrassCurve.Affine.Point instAdd some instNeg WeierstrassCurve.Affine.addX WeierstrassCurve.Affine.slope WeierstrassCurve.Affine.negAddY WeierstrassCurve.Affine.nonsingular_negAdd WeierstrassCurve.Affine.negY	—	add_of_Y_ne
add_self_of_Y_eq 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Affine.negY	WeierstrassCurve.Affine.Point instAdd some instZero	—	add_of_Y_eq
add_self_of_Y_ne 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	WeierstrassCurve.Affine.Point instAdd some WeierstrassCurve.Affine.addX WeierstrassCurve.Affine.slope WeierstrassCurve.Affine.addY WeierstrassCurve.Affine.nonsingular_add WeierstrassCurve.Affine.negY	—	add_of_Y_ne
add_self_of_Y_ne' 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	WeierstrassCurve.Affine.Point instAdd some instNeg WeierstrassCurve.Affine.addX WeierstrassCurve.Affine.slope WeierstrassCurve.Affine.negAddY WeierstrassCurve.Affine.nonsingular_negAdd WeierstrassCurve.Affine.negY	—	add_of_Y_ne
add_some 📖	mathematical	WeierstrassCurve.Affine.negY EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Affine.Nonsingular	WeierstrassCurve.Affine.Point instAdd some WeierstrassCurve.Affine.addX WeierstrassCurve.Affine.slope WeierstrassCurve.Affine.addY WeierstrassCurve.Affine.nonsingular_add	—	WeierstrassCurve.Affine.nonsingular_add
map_baseChange 📖	mathematical	—	DFunLike.coe AddMonoidHom WeierstrassCurve.Affine.Point EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.baseChange AddZeroClass.toAddZero instAddZeroClass AddMonoidHom.instFunLike map baseChange	—	AlgHom.subsingleton Unique.instSubsingleton IsScalarTower.right Lean.Meta.FastSubsingleton.elim Lean.Meta.instFastSubsingletonForall Lean.Meta.instFastSubsingletonDecidable map_map
map_id 📖	mathematical	—	DFunLike.coe AddMonoidHom WeierstrassCurve.Affine.Point EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.baseChange AddZeroClass.toAddZero instAddZeroClass AddMonoidHom.instFunLike map Algebra.id Semifield.toCommSemiring Field.toSemifield IsScalarTower.right CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Algebra.ofId	—	IsScalarTower.right
map_injective 📖	mathematical	—	WeierstrassCurve.Affine.Point EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.baseChange DFunLike.coe AddMonoidHom AddZeroClass.toAddZero instAddZeroClass AddMonoidHom.instFunLike map	—	RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing
map_map 📖	mathematical	—	DFunLike.coe AddMonoidHom WeierstrassCurve.Affine.Point EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.baseChange AddZeroClass.toAddZero instAddZeroClass AddMonoidHom.instFunLike map AlgHom.comp CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	—
map_some 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.toAffine WeierstrassCurve.baseChange	DFunLike.coe AddMonoidHom WeierstrassCurve.Affine.Point AddZeroClass.toAddZero instAddZeroClass AddMonoidHom.instFunLike map some AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike WeierstrassCurve.Affine.baseChange_nonsingular RingHom.injective NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing DivisionRing.isSimpleRing Field.toDivisionRing Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.toNontrivial Field.instIsLocalRing AlgHom.toRingHom	—	—
map_zero 📖	mathematical	—	DFunLike.coe AddMonoidHom WeierstrassCurve.Affine.Point EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.baseChange AddZeroClass.toAddZero instAddZeroClass AddMonoidHom.instFunLike map instZero	—	—
neg_def 📖	mathematical	—	WeierstrassCurve.Affine.Point instNeg neg	—	—
neg_some 📖	mathematical	WeierstrassCurve.Affine.Nonsingular	WeierstrassCurve.Affine.Point instNeg some WeierstrassCurve.Affine.negY WeierstrassCurve.Affine.nonsingular_neg	—	—
neg_zero 📖	mathematical	—	WeierstrassCurve.Affine.Point instNeg instZero	—	—
some_ne_zero 📖	—	WeierstrassCurve.Affine.Nonsingular	—	—	—
toClass_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom WeierstrassCurve.Affine.Point EuclideanDomain.toCommRing Field.toEuclideanDomain Additive ClassGroup WeierstrassCurve.Affine.CoordinateRing AdjoinRoot.instCommRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing WeierstrassCurve.Affine.polynomial WeierstrassCurve.Affine.CoordinateRing.instIsDomain instIsDomain Field.toSemifield AddZeroClass.toAddZero instAddZeroClass Additive.addZeroClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup AddMonoidHom.instFunLike toClass instZeroAdditiveOfOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul MonoidHom Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero WeierstrassCurve.Affine.FunctionField FractionRing.field OreLocalization.instAlgebra OreLocalization.oreSetComm CommRing.toCommMonoid Algebra.id MonoidWithZero.toMonoid FractionalIdeal.commSemiring MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike WeierstrassCurve.Affine.CoordinateRing.XYIdeal'	—	WeierstrassCurve.Affine.CoordinateRing.instIsDomain instIsDomain
toClass_eq_zero 📖	mathematical	—	DFunLike.coe AddMonoidHom WeierstrassCurve.Affine.Point EuclideanDomain.toCommRing Field.toEuclideanDomain Additive ClassGroup WeierstrassCurve.Affine.CoordinateRing AdjoinRoot.instCommRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing WeierstrassCurve.Affine.polynomial WeierstrassCurve.Affine.CoordinateRing.instIsDomain instIsDomain Field.toSemifield AddZeroClass.toAddZero instAddZeroClass Additive.addZeroClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup AddMonoidHom.instFunLike toClass instZeroAdditiveOfOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid instZero	—	WeierstrassCurve.Affine.CoordinateRing.instIsDomain instIsDomain Localization.isLocalization ClassGroup.mk_eq_one_of_coe_ideal WeierstrassCurve.Affine.CoordinateRing.natDegree_norm_ne_one IsScalarTower.right finrank_quotient_span_eq_natDegree_norm Finite.of_fintype WeierstrassCurve.Affine.CoordinateRing.instIsScalarTowerPolynomial Ideal.instIsTwoSided_1 LinearEquiv.finrank_eq Module.finrank_self commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing
toClass_injective 📖	mathematical	—	WeierstrassCurve.Affine.Point EuclideanDomain.toCommRing Field.toEuclideanDomain Additive ClassGroup WeierstrassCurve.Affine.CoordinateRing AdjoinRoot.instCommRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing WeierstrassCurve.Affine.polynomial WeierstrassCurve.Affine.CoordinateRing.instIsDomain instIsDomain Field.toSemifield DFunLike.coe AddMonoidHom AddZeroClass.toAddZero instAddZeroClass Additive.addZeroClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup AddMonoidHom.instFunLike toClass	—	WeierstrassCurve.Affine.CoordinateRing.instIsDomain instIsDomain toClass_eq_zero map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass zero_add WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul
toClass_some 📖	mathematical	WeierstrassCurve.Affine.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	DFunLike.coe AddMonoidHom WeierstrassCurve.Affine.Point Additive ClassGroup WeierstrassCurve.Affine.CoordinateRing AdjoinRoot.instCommRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing WeierstrassCurve.Affine.polynomial WeierstrassCurve.Affine.CoordinateRing.instIsDomain instIsDomain Field.toSemifield AddZeroClass.toAddZero instAddZeroClass Additive.addZeroClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup AddMonoidHom.instFunLike toClass some MonoidHom Units FractionalIdeal nonZeroDivisors Semiring.toMonoidWithZero WeierstrassCurve.Affine.FunctionField FractionRing.field OreLocalization.instAlgebra OreLocalization.oreSetComm CommRing.toCommMonoid Algebra.id MonoidWithZero.toMonoid FractionalIdeal.commSemiring MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Localization.isLocalization WeierstrassCurve.Affine.CoordinateRing.XYIdeal'	—	WeierstrassCurve.Affine.CoordinateRing.instIsDomain instIsDomain
toClass_zero 📖	mathematical	—	DFunLike.coe AddMonoidHom WeierstrassCurve.Affine.Point EuclideanDomain.toCommRing Field.toEuclideanDomain Additive ClassGroup WeierstrassCurve.Affine.CoordinateRing AdjoinRoot.instCommRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing WeierstrassCurve.Affine.polynomial WeierstrassCurve.Affine.CoordinateRing.instIsDomain instIsDomain Field.toSemifield AddZeroClass.toAddZero instAddZeroClass Additive.addZeroClass Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid CommGroup.toGroup instCommGroupClassGroup AddMonoidHom.instFunLike toClass instZero instZeroAdditiveOfOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	WeierstrassCurve.Affine.CoordinateRing.instIsDomain instIsDomain
zero_def 📖	mathematical	—	WeierstrassCurve.Affine.Point instZero zero	—	—

---

← Back to Index