Theorems · Theorem · algebraic geometry
WeierstrassCurve.Jacobian.equiv_some_of_Z_ne_zero
∀ {F : Type u} [inst : Field F] {P : Fin 3 → F}, P 2 ≠ 0 → P ≈ ![P 0 / P 2 ^ 2, P 1 / P 2 ^ 3, 1]- Cited by
- 2 results in Mathlib
- Foundations
- Depth 68 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement and proof · cited by 7,404
- Nat.cast_oneproof · cited by 2,501
- Nat.cast_zeroproof · cited by 1,870
- one_ne_zeroproof · cited by 885
- Matrix.vecConsstatement and proof · cited by 852
- Matrix.vecEmptystatement and proof · cited by 832
- div_selfproof · cited by 237
- pow_ne_zeroproof · cited by 208
- Matrix.vecHeadproof · cited by 34
- Matrix.tail_consproof · cited by 16
- WeierstrassCurve.Jacobian.equiv_of_X_eq_of_Y_eqproof · cited by 4
Cited by2
Results whose statement or proof uses this declaration.
- WeierstrassCurve.Jacobian.nonsingular_of_Z_ne_zeroproof · cited by 7
- WeierstrassCurve.Jacobian.equation_of_Z_ne_zeroproof · cited by 1