Z_eq_zero_of_equiv

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

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

← MathLib Explorer

English

If P ≈ Q then P z = 0 iff Q z = 0.

Русский

Если P эквивалентно Q, то P z = 0 тогда и только тогда, когда Q z = 0.

LaTeX

$$P ≈ Q ⇒ (P z = 0) ⇔ (Q z = 0)$$

Lean4

theorem Z_eq_zero_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : P z = 0 ↔ Q z = 0 :=
  by
  rcases h with ⟨_, rfl⟩
  simp only [Units.smul_def, smul_fin3_ext, Units.mul_right_eq_zero]

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

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

Разделы

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

Аффилиация

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