Point

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

Statistics

Metric	Count
Definitions Point, toProjective, Point, add, fromAffine, instAdd, instAddCommGroup, instNeg, instZeroOfNontrivial, neg, point, toAffine, toAffineAddEquiv, toAffineLift, add, addMap, neg, negMap	18
Theorems add_def, add_point, ext, ext_iff, fromAffine_some, fromAffine_some_ne_zero, fromAffine_zero, mk_ne_zero, mk_point, neg_def, neg_point, nonsingular, toAffineAddEquiv_apply, toAffineAddEquiv_symm_apply, toAffineLift_add, toAffineLift_eq, toAffineLift_neg, toAffineLift_of_Z_eq_zero, toAffineLift_of_Z_ne_zero, toAffineLift_some, toAffineLift_zero, toAffine_add, toAffine_neg, toAffine_of_Z_eq_zero, toAffine_of_Z_ne_zero, toAffine_of_equiv, toAffine_of_singular, toAffine_smul, toAffine_some, toAffine_zero, zero_def, zero_point, addMap_eq, addMap_of_Y_eq, addMap_of_Z_eq_zero_left, addMap_of_Z_eq_zero_right, addMap_of_Z_ne_zero, addXYZ_neg, addX_neg, addY_neg, addZ_neg, add_equiv, add_of_X_ne, add_of_Y_eq, add_of_Y_ne, add_of_Y_ne', add_of_Z_eq_zero, add_of_Z_eq_zero_left, add_of_Z_eq_zero_right, add_of_eq, add_of_equiv, add_of_not_equiv, add_self, add_smul_equiv, add_smul_of_equiv, add_smul_of_not_equiv, baseChange_add, baseChange_neg, map_add, map_neg, negAddY_neg, negMap_eq, negMap_of_Z_eq_zero, negMap_of_Z_ne_zero, neg_X, neg_Y, neg_Z, neg_equiv, neg_of_Z_eq_zero, neg_of_Z_ne_zero, neg_smul, neg_smul_equiv, nonsingularLift_addMap, nonsingularLift_negMap, nonsingular_add, nonsingular_neg	76
Total	94

CategoryTheory.GrothendieckTopology

Definitions

Name	Category	Theorems
Point 📖	CompData	9 math math: Point.id_hom, Point.Hom.presheafFiber_comp, Point.Hom.sheafFiber_comp_assoc, Point.Hom.presheafFiber_comp_assoc, Point.Hom.sheafFiber_comp, Point.Hom.presheafFiber_id, Point.comp_hom, Point.Hom.sheafFiber_id, Point.comp_hom_assoc

WeierstrassCurve.Affine.Point

Definitions

Name	Category	Theorems
toProjective 📖	CompOp	—

WeierstrassCurve.Projective

Definitions

Name	Category	Theorems
Point 📖	CompData	12 math math: Point.zero_point, Point.toAffineAddEquiv_apply, Point.toAffineLift_neg, Point.toAffineLift_zero, Point.neg_point, Point.neg_def, Point.toAffineLift_add, Point.zero_def, Point.add_def, Point.add_point, Point.fromAffine_zero, Point.toAffineAddEquiv_symm_apply
add 📖	CompOp	20 math math: add_of_Z_eq_zero, add_equiv, add_of_Z_eq_zero_left, addMap_eq, add_of_equiv, add_self, add_of_Z_eq_zero_right, nonsingular_add, baseChange_add, add_smul_equiv, add_smul_of_not_equiv, add_of_Y_eq, add_of_X_ne, add_of_Y_ne', Point.toAffine_add, add_of_not_equiv, add_smul_of_equiv, map_add, add_of_eq, add_of_Y_ne
addMap 📖	CompOp	7 math math: addMap_of_Z_eq_zero_left, addMap_eq, nonsingularLift_addMap, addMap_of_Y_eq, addMap_of_Z_eq_zero_right, addMap_of_Z_ne_zero, Point.add_point
neg 📖	CompOp	18 math math: map_neg, addY_neg, nonsingular_neg, neg_equiv, neg_Y, neg_X, addX_neg, addXYZ_neg, negAddY_neg, Point.toAffine_neg, neg_of_Z_ne_zero, negMap_eq, neg_of_Z_eq_zero, neg_smul, baseChange_neg, addZ_neg, neg_Z, neg_smul_equiv
negMap 📖	CompOp	5 math math: Point.neg_point, negMap_of_Z_ne_zero, negMap_eq, negMap_of_Z_eq_zero, nonsingularLift_negMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addMap_eq 📖	mathematical	—	addMap MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule add	—	—
addMap_of_Y_eq 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain Equation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negY	addMap MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Module.toDistribMulAction Semiring.toModule Matrix.vecCons MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.vecEmpty	—	addMap_eq add_of_Y_eq smul_eq isUnit_dblU_of_Y_eq add_of_Y_ne isUnit_addU_of_Y_ne
addMap_of_Z_eq_zero_left 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain NonsingularLift MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addMap MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Module.toDistribMulAction Semiring.toModule	—	addMap_eq add_of_Z_eq_zero smul_eq IsUnit.pow isUnit_Y_of_Z_eq_zero Quotient.eq equiv_zero_of_Z_eq_zero add_of_Z_eq_zero_left IsDomain.to_noZeroDivisors instIsDomain IsUnit.mul Ne.isUnit
addMap_of_Z_eq_zero_right 📖	mathematical	NonsingularLift EuclideanDomain.toCommRing Field.toEuclideanDomain Nonsingular MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	addMap MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Module.toDistribMulAction Semiring.toModule	—	addMap_eq add_of_Z_eq_zero smul_eq IsUnit.pow isUnit_Y_of_Z_eq_zero Quotient.eq equiv_zero_of_Z_eq_zero add_of_Z_eq_zero_right IsDomain.to_noZeroDivisors instIsDomain IsUnit.neg IsUnit.mul Ne.isUnit
addMap_of_Z_ne_zero 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negY	addMap MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Module.toDistribMulAction Semiring.toModule Matrix.vecCons WeierstrassCurve.Affine.addX toAffine DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing WeierstrassCurve.Affine.slope WeierstrassCurve.Affine.addY AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Matrix.vecEmpty	—	addMap_eq add_of_Y_ne' smul_eq isUnit_dblZ_of_Y_ne' add_of_X_ne isUnit_addZ_of_X_ne
addXYZ_neg 📖	mathematical	Equation	addXYZ neg Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing dblZ Matrix.vecCons MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Matrix.vecEmpty	—	addXYZ.eq_1 addX_neg addY_neg addZ_neg smul_fin3 MulZeroClass.mul_zero mul_one
addX_neg 📖	mathematical	—	addX neg MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	addX.eq_1 neg_X neg_Y neg_Z negY.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_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.pow_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right 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.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_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.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
addY_neg 📖	mathematical	Equation	addY neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing dblZ	—	addX_neg negAddY_neg addZ_neg MulZeroClass.mul_zero sub_zero
addZ_neg 📖	mathematical	—	addZ neg MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	addZ.eq_1 neg_X neg_Y neg_Z negY.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.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.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.add_pf_zero_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt 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 Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.cast_zero Nat.cast_zero
add_equiv 📖	mathematical	instSetoidForallFinOfNatNat	add	—	add_smul_equiv Units.isUnit
add_of_X_ne 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain	add Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id addZ Matrix.vecCons WeierstrassCurve.Affine.addX toAffine DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing WeierstrassCurve.Affine.slope WeierstrassCurve.Affine.addY AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Matrix.vecEmpty	—	add_of_not_equiv not_equiv_of_X_ne addXYZ_of_Z_ne_zero
add_of_Y_eq 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing negY	add Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id dblU Matrix.vecCons MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.vecEmpty	—	add_of_equiv equiv_of_X_eq_of_Y_eq dblXYZ_of_Y_eq
add_of_Y_ne 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	add Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id addU Matrix.vecCons MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.vecEmpty	—	add_of_not_equiv not_equiv_of_Y_ne addXYZ_of_X_eq
add_of_Y_ne' 📖	mathematical	Equation EuclideanDomain.toCommRing Field.toEuclideanDomain Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	add Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id dblZ Matrix.vecCons WeierstrassCurve.Affine.addX toAffine DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing WeierstrassCurve.Affine.slope WeierstrassCurve.Affine.addY AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Matrix.vecEmpty	—	add_of_equiv equiv_of_X_eq_of_Y_eq Y_eq_of_Y_ne' IsDomain.to_noZeroDivisors instIsDomain dblXYZ_of_Z_ne_zero
add_of_Z_eq_zero 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	add Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.vecEmpty	—	add_of_equiv equiv_of_Z_eq_zero dblXYZ_of_Z_eq_zero IsDomain.to_noZeroDivisors instIsDomain
add_of_Z_eq_zero_left 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	add Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	add_of_not_equiv not_equiv_of_Z_eq_zero_left addXYZ_of_Z_eq_zero_left
add_of_Z_eq_zero_right 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	add Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	add_of_not_equiv not_equiv_of_Z_eq_zero_right addXYZ_of_Z_eq_zero_right
add_of_eq 📖	mathematical	—	add dblXYZ	—	add_self
add_of_equiv 📖	mathematical	instSetoidForallFinOfNatNat	add dblXYZ	—	—
add_of_not_equiv 📖	mathematical	instSetoidForallFinOfNatNat	add addXYZ	—	—
add_self 📖	mathematical	—	add dblXYZ	—	add_of_equiv
add_smul_equiv 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	instSetoidForallFinOfNatNat add Function.hasSMul Algebra.toSMul Algebra.id	—	add_smul_of_equiv add_smul_of_not_equiv
add_smul_of_equiv 📖	mathematical	instSetoidForallFinOfNatNat IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	add Function.hasSMul Algebra.toSMul Algebra.id Monoid.toNatPow	—	add_of_equiv smul_equiv_smul dblXYZ_smul
add_smul_of_not_equiv 📖	mathematical	instSetoidForallFinOfNatNat IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	add Function.hasSMul Algebra.toSMul Algebra.id Monoid.toNatPow Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	add_of_not_equiv smul_equiv_smul addXYZ_smul
baseChange_add 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.toProjective WeierstrassCurve.baseChange	add DFunLike.coe AlgHom CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_add WeierstrassCurve.map_baseChange
baseChange_neg 📖	mathematical	—	neg WeierstrassCurve.toProjective WeierstrassCurve.baseChange DFunLike.coe AlgHom CommRing.toCommSemiring CommSemiring.toSemiring AlgHom.funLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.coe_coe map_neg WeierstrassCurve.map_baseChange
map_add 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	add WeierstrassCurve.toProjective WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike	—	add_of_equiv comp_equiv_comp map_dblXYZ add_of_not_equiv map_addXYZ
map_neg 📖	mathematical	—	neg WeierstrassCurve.toProjective WeierstrassCurve.map DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike	—	map_negY comp_fin3
negAddY_neg 📖	mathematical	Equation	negAddY neg dblZ	—	Mathlib.Tactic.LinearCombination.eq_of_eq Nat.instAtLeastTwoHAddOfNat AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.LinearCombination.mul_const_eq equation_iff Mathlib.Tactic.LinearCombination.eq_rearrange negAddY.eq_1 neg_X neg_Y neg_Z dblZ.eq_1 negY.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo 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.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.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf 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.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.pow_bit1 Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero
negMap_eq 📖	mathematical	—	negMap MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule neg	—	—
negMap_of_Z_eq_zero 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	negMap MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Module.toDistribMulAction Semiring.toModule Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.vecEmpty	—	negMap_eq neg_of_Z_eq_zero IsDomain.to_noZeroDivisors instIsDomain smul_eq IsUnit.neg isUnit_Y_of_Z_eq_zero
negMap_of_Z_ne_zero 📖	mathematical	—	negMap EuclideanDomain.toCommRing Field.toEuclideanDomain MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule Matrix.vecCons DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing WeierstrassCurve.Affine.negY toAffine AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Matrix.vecEmpty	—	negMap_eq neg_of_Z_ne_zero smul_eq Ne.isUnit
neg_X 📖	mathematical	—	neg	—	—
neg_Y 📖	mathematical	—	neg negY	—	—
neg_Z 📖	mathematical	—	neg	—	—
neg_equiv 📖	mathematical	instSetoidForallFinOfNatNat	neg	—	neg_smul_equiv Units.isUnit
neg_of_Z_eq_zero 📖	mathematical	Equation MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	neg Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Matrix.vecEmpty	—	X_eq_zero_of_Z_eq_zero negY_of_Z_eq_zero neg_smul Matrix.smul_cons MulZeroClass.mul_zero mul_one Matrix.smul_empty Matrix.neg_cons neg_zero Matrix.neg_empty
neg_of_Z_ne_zero 📖	mathematical	—	neg EuclideanDomain.toCommRing Field.toEuclideanDomain Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id Matrix.vecCons DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing WeierstrassCurve.Affine.negY toAffine AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Matrix.vecEmpty	—	neg.eq_1 smul_fin3 mul_div_cancel₀ negY_of_Z_ne_zero mul_one
neg_smul 📖	mathematical	—	neg Function.hasSMul Algebra.toSMul CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id	—	negY_smul smul_fin3
neg_smul_equiv 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring	instSetoidForallFinOfNatNat neg Function.hasSMul Algebra.toSMul Algebra.id	—	neg_smul
nonsingularLift_addMap 📖	mathematical	NonsingularLift EuclideanDomain.toCommRing Field.toEuclideanDomain	addMap	—	nonsingular_add
nonsingularLift_negMap 📖	mathematical	NonsingularLift EuclideanDomain.toCommRing Field.toEuclideanDomain	negMap	—	nonsingular_neg
nonsingular_add 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	add	—	add_of_Z_eq_zero nonsingular_smul IsUnit.pow isUnit_Y_of_Z_eq_zero IsLocalRing.toNontrivial Field.instIsLocalRing add_of_Z_eq_zero_left IsDomain.to_noZeroDivisors instIsDomain IsUnit.mul Ne.isUnit add_of_Z_eq_zero_right IsUnit.neg add_of_Y_eq isUnit_dblU_of_Y_eq add_of_Y_ne isUnit_addU_of_Y_ne add_of_Y_ne' isUnit_dblZ_of_Y_ne' add_of_X_ne isUnit_addZ_of_X_ne
nonsingular_neg 📖	mathematical	Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	neg	—	neg_of_Z_eq_zero IsDomain.to_noZeroDivisors instIsDomain nonsingular_smul IsUnit.neg isUnit_Y_of_Z_eq_zero IsLocalRing.toNontrivial Field.instIsLocalRing neg_of_Z_ne_zero Ne.isUnit

WeierstrassCurve.Projective.Point

Definitions

Name	Category	Theorems
add 📖	CompOp	1 math math: add_def
fromAffine 📖	CompOp	3 math math: fromAffine_some, fromAffine_zero, toAffineAddEquiv_symm_apply
instAdd 📖	CompOp	5 math math: toAffineAddEquiv_apply, toAffineLift_add, add_def, add_point, toAffineAddEquiv_symm_apply
instAddCommGroup 📖	CompOp	—
instNeg 📖	CompOp	3 math math: toAffineLift_neg, neg_point, neg_def
instZeroOfNontrivial 📖	CompOp	4 math math: zero_point, toAffineLift_zero, zero_def, fromAffine_zero
neg 📖	CompOp	1 math math: neg_def
point 📖	CompOp	6 math math: zero_point, nonsingular, mk_point, ext_iff, neg_point, add_point
toAffine 📖	CompOp	10 math math: toAffine_smul, toAffine_some, toAffine_of_singular, toAffine_neg, toAffine_of_Z_ne_zero, toAffine_add, toAffine_of_Z_eq_zero, toAffine_zero, toAffineLift_eq, toAffine_of_equiv
toAffineAddEquiv 📖	CompOp	2 math math: toAffineAddEquiv_apply, toAffineAddEquiv_symm_apply
toAffineLift 📖	CompOp	8 math math: toAffineLift_of_Z_ne_zero, toAffineAddEquiv_apply, toAffineLift_neg, toAffineLift_zero, toAffineLift_of_Z_eq_zero, toAffineLift_some, toAffineLift_add, toAffineLift_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_def 📖	mathematical	—	WeierstrassCurve.Projective.Point EuclideanDomain.toCommRing Field.toEuclideanDomain instAdd add	—	—
add_point 📖	mathematical	—	point EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Projective.Point instAdd WeierstrassCurve.Projective.addMap	—	—
ext 📖	—	point	—	—	—
ext_iff 📖	mathematical	—	point	—	ext
fromAffine_some 📖	mathematical	WeierstrassCurve.Affine.Nonsingular WeierstrassCurve.Projective.toAffine	fromAffine WeierstrassCurve.Affine.Point.some MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.vecEmpty WeierstrassCurve.Projective.NonsingularLift WeierstrassCurve.Projective.nonsingularLift_some	—	—
fromAffine_some_ne_zero 📖	—	WeierstrassCurve.Affine.Nonsingular WeierstrassCurve.Projective.toAffine	—	—	mk_ne_zero WeierstrassCurve.Projective.nonsingularLift_some
fromAffine_zero 📖	mathematical	—	fromAffine WeierstrassCurve.Affine.Point WeierstrassCurve.Projective.toAffine WeierstrassCurve.Affine.Point.instZero WeierstrassCurve.Projective.Point instZeroOfNontrivial	—	—
mk_ne_zero 📖	—	WeierstrassCurve.Projective.NonsingularLift MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.vecEmpty	—	—	WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_right one_ne_zero NeZero.one Quotient.eq ext_iff
mk_point 📖	mathematical	WeierstrassCurve.Projective.NonsingularLift	point	—	—
neg_def 📖	mathematical	—	WeierstrassCurve.Projective.Point EuclideanDomain.toCommRing Field.toEuclideanDomain instNeg neg	—	—
neg_point 📖	mathematical	—	point EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Projective.Point instNeg WeierstrassCurve.Projective.negMap	—	—
nonsingular 📖	mathematical	—	WeierstrassCurve.Projective.NonsingularLift point	—	—
toAffineAddEquiv_apply 📖	mathematical	—	DFunLike.coe AddEquiv WeierstrassCurve.Projective.Point EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Affine.Point WeierstrassCurve.Projective.toAffine instAdd WeierstrassCurve.Affine.Point.instAdd EquivLike.toFunLike AddEquiv.instEquivLike toAffineAddEquiv toAffineLift	—	—
toAffineAddEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv WeierstrassCurve.Affine.Point EuclideanDomain.toCommRing Field.toEuclideanDomain WeierstrassCurve.Projective.toAffine WeierstrassCurve.Projective.Point WeierstrassCurve.Affine.Point.instAdd instAdd EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm toAffineAddEquiv fromAffine	—	—
toAffineLift_add 📖	mathematical	—	toAffineLift WeierstrassCurve.Projective.Point EuclideanDomain.toCommRing Field.toEuclideanDomain instAdd WeierstrassCurve.Affine.Point WeierstrassCurve.Projective.toAffine WeierstrassCurve.Affine.Point.instAdd	—	toAffine_add
toAffineLift_eq 📖	mathematical	WeierstrassCurve.Projective.NonsingularLift EuclideanDomain.toCommRing Field.toEuclideanDomain MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule	toAffineLift toAffine	—	—
toAffineLift_neg 📖	mathematical	—	toAffineLift WeierstrassCurve.Projective.Point EuclideanDomain.toCommRing Field.toEuclideanDomain instNeg WeierstrassCurve.Affine.Point WeierstrassCurve.Projective.toAffine WeierstrassCurve.Affine.Point.instNeg	—	toAffine_neg
toAffineLift_of_Z_eq_zero 📖	mathematical	WeierstrassCurve.Projective.NonsingularLift EuclideanDomain.toCommRing Field.toEuclideanDomain MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	toAffineLift WeierstrassCurve.Affine.Point WeierstrassCurve.Projective.toAffine WeierstrassCurve.Affine.Point.instZero	—	toAffine_of_Z_eq_zero
toAffineLift_of_Z_ne_zero 📖	mathematical	WeierstrassCurve.Projective.NonsingularLift EuclideanDomain.toCommRing Field.toEuclideanDomain MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule	toAffineLift WeierstrassCurve.Affine.Point.some WeierstrassCurve.Projective.toAffine DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing WeierstrassCurve.Projective.Nonsingular WeierstrassCurve.Affine.Nonsingular WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero	—	toAffine_of_Z_ne_zero
toAffineLift_some 📖	mathematical	WeierstrassCurve.Projective.NonsingularLift EuclideanDomain.toCommRing Field.toEuclideanDomain MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.vecEmpty	toAffineLift WeierstrassCurve.Affine.Point.some WeierstrassCurve.Projective.toAffine WeierstrassCurve.Projective.Nonsingular CommRing.toRing WeierstrassCurve.Affine.Nonsingular WeierstrassCurve.Projective.nonsingular_some	—	toAffine_some
toAffineLift_zero 📖	mathematical	—	toAffineLift WeierstrassCurve.Projective.Point EuclideanDomain.toCommRing Field.toEuclideanDomain instZeroOfNontrivial IsLocalRing.toNontrivial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Field.instIsLocalRing WeierstrassCurve.Affine.Point WeierstrassCurve.Projective.toAffine WeierstrassCurve.Affine.Point.instZero	—	toAffine_zero
toAffine_add 📖	mathematical	WeierstrassCurve.Projective.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	toAffine WeierstrassCurve.Projective.add WeierstrassCurve.Affine.Point WeierstrassCurve.Projective.toAffine WeierstrassCurve.Affine.Point.instAdd	—	toAffine_of_Z_eq_zero zero_add WeierstrassCurve.Projective.add_of_Z_eq_zero toAffine_smul IsUnit.pow WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero toAffine_zero WeierstrassCurve.Projective.add_of_Z_eq_zero_left IsDomain.to_noZeroDivisors instIsDomain IsUnit.mul Ne.isUnit WeierstrassCurve.Projective.add_of_Z_eq_zero_right IsUnit.neg add_zero WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero toAffine_of_Z_ne_zero WeierstrassCurve.Affine.Point.add_of_Y_eq WeierstrassCurve.Projective.X_eq_iff WeierstrassCurve.Projective.Y_eq_iff' WeierstrassCurve.Projective.add_of_Y_eq WeierstrassCurve.Projective.isUnit_dblU_of_Y_eq WeierstrassCurve.Projective.add_of_Y_ne WeierstrassCurve.Projective.isUnit_addU_of_Y_ne WeierstrassCurve.Projective.add_of_Y_ne' WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne' WeierstrassCurve.Projective.add_of_X_ne WeierstrassCurve.Projective.isUnit_addZ_of_X_ne
toAffine_neg 📖	mathematical	WeierstrassCurve.Projective.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	toAffine WeierstrassCurve.Projective.neg WeierstrassCurve.Affine.Point WeierstrassCurve.Projective.toAffine WeierstrassCurve.Affine.Point.instNeg	—	WeierstrassCurve.Projective.neg_of_Z_eq_zero IsDomain.to_noZeroDivisors instIsDomain toAffine_smul IsUnit.neg WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero toAffine_zero toAffine_of_Z_eq_zero WeierstrassCurve.Affine.Point.neg_zero WeierstrassCurve.Projective.neg_of_Z_ne_zero Ne.isUnit WeierstrassCurve.Projective.nonsingular_some WeierstrassCurve.Projective.nonsingular_smul WeierstrassCurve.Projective.nonsingular_neg toAffine_some WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero toAffine_of_Z_ne_zero WeierstrassCurve.Affine.nonsingular_neg WeierstrassCurve.Affine.Point.neg_some
toAffine_of_Z_eq_zero 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	toAffine WeierstrassCurve.Affine.Point WeierstrassCurve.Projective.toAffine WeierstrassCurve.Affine.Point.instZero	—	toAffine.eq_1 not_and_not_right
toAffine_of_Z_ne_zero 📖	mathematical	WeierstrassCurve.Projective.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	toAffine WeierstrassCurve.Affine.Point.some WeierstrassCurve.Projective.toAffine DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing WeierstrassCurve.Affine.Nonsingular WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero	—	WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero toAffine.eq_1
toAffine_of_equiv 📖	mathematical	WeierstrassCurve.Projective.instSetoidForallFinOfNatNat EuclideanDomain.toCommRing Field.toEuclideanDomain	toAffine	—	toAffine_smul Units.isUnit
toAffine_of_singular 📖	mathematical	WeierstrassCurve.Projective.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain	toAffine WeierstrassCurve.Affine.Point WeierstrassCurve.Projective.toAffine WeierstrassCurve.Affine.Point.instZero	—	toAffine.eq_1
toAffine_smul 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	toAffine Function.hasSMul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id	—	toAffine_of_Z_eq_zero mul_eq_zero_of_right WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero mul_ne_zero IsDomain.to_noZeroDivisors instIsDomain IsUnit.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing WeierstrassCurve.Projective.nonsingular_smul toAffine_of_Z_ne_zero mul_div_mul_left toAffine_of_singular
toAffine_some 📖	mathematical	WeierstrassCurve.Projective.Nonsingular EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix.vecCons AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.vecEmpty	toAffine WeierstrassCurve.Affine.Point.some WeierstrassCurve.Projective.toAffine CommRing.toRing WeierstrassCurve.Affine.Nonsingular WeierstrassCurve.Projective.nonsingular_some	—	WeierstrassCurve.Projective.nonsingular_some WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero one_ne_zero NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing div_one toAffine_of_Z_ne_zero WeierstrassCurve.Affine.Point.some.congr_simp
toAffine_zero 📖	mathematical	—	toAffine Matrix.vecCons MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing Matrix.vecEmpty WeierstrassCurve.Affine.Point WeierstrassCurve.Projective.toAffine WeierstrassCurve.Affine.Point.instZero	—	toAffine_of_Z_eq_zero
zero_def 📖	mathematical	—	WeierstrassCurve.Projective.Point instZeroOfNontrivial MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule Matrix.vecCons MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.vecEmpty WeierstrassCurve.Projective.nonsingularLift_zero	—	—
zero_point 📖	mathematical	—	point WeierstrassCurve.Projective.Point instZeroOfNontrivial MulAction.orbitRel Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Units.instGroup Units.instMulAction Pi.mulAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Semiring.toModule Matrix.vecCons MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Matrix.vecEmpty	—	—

---

← Back to Index