smul_equiv

Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic

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

English

For P,Q: Fin 3 → R and unit elements u,v, the relation u • P ≈ v • Q holds iff P ≈ Q.

Русский

Для P,Q: Fin 3 → R и единиц u, v тогда u • P ≈ v • Q тогда выполняется тогда, когда P ≈ Q.

LaTeX

$$$u \cdot P \;\approx\; v \cdot Q \;\iff\; P \approx Q$$$

Lean4

theorem smul_equiv (P : Fin 3 → R) {u : R} (hu : IsUnit u) : u • P ≈ P :=
  ⟨hu.unit, rfl⟩

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

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

Разделы

Аффилиация

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