Theorems · Theorem · algebraic geometry
WeierstrassCurve.Projective.smul_fin3
∀ {R : Type r} [inst : CommRing R] (P : Fin 3 → R) (u : R), u • P = ![u * P 0, u * P 1, u * P 2]- Cited by
- 14 results in Mathlib
- Foundations
- Depth 54 from the axioms · uses propext, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Matrix.vecConsstatement and proof · cited by 852
- Matrix.vecEmptystatement and proof · cited by 832
- Matrix.cons_val_fin_oneproof · cited by 225
- Matrix.cons_val_succproof · cited by 47
Cited by14
Results whose statement or proof uses this declaration.
- WeierstrassCurve.Projective.equiv_of_X_eq_of_Y_eqproof · cited by 4
- WeierstrassCurve.Projective.neg_of_Z_ne_zeroproof · cited by 3
- WeierstrassCurve.Projective.equiv_of_Z_eq_zeroproof · cited by 3
- WeierstrassCurve.Projective.addXYZ_of_X_eqproof · cited by 1
- WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_leftproof · cited by 1
- WeierstrassCurve.Projective.addXYZ_of_Z_eq_zero_rightproof · cited by 1
- WeierstrassCurve.Projective.addXYZ_of_Z_ne_zeroproof · cited by 1
- WeierstrassCurve.Projective.neg_smulproof · cited by 1
- WeierstrassCurve.Projective.addXYZ_smulproof · cited by 1
- WeierstrassCurve.Projective.dblXYZ_of_Y_eqproof · cited by 1
- WeierstrassCurve.Projective.dblXYZ_of_Z_eq_zeroproof · cited by 1
- WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zeroproof · cited by 1