smul_equiv_smul

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.Projective.smul_equiv_smul

← MathLib Explorer

English

If P ≈ Q, then P x · Q z = Q x · P z.

Русский

Если P эквивалентно Q, то P x Q z = Q x P z.

LaTeX

$$P(0)·Q(2) = Q(0)·P(2)$$

Lean4

theorem smul_equiv_smul (P Q : Fin 3 → R) {u v : R} (hu : IsUnit u) (hv : IsUnit v) : u • P ≈ v • Q ↔ P ≈ Q := by
  rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv, smul_eq P hu, smul_eq Q hv]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru