map_j

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.map_j

English

Under a ring hom f, the j-invariant commutes with base change: (W.map f).j = f(W.j).

Русский

При базисном переносе по f j-инвариант коммутирует с образом: j(W.map f) = f(j(W)).

LaTeX

$$(W.map f).j = f(W.j)$$

Lean4

@[simp]
theorem map_j : (W.map f).j = f W.j := by rw [j, coe_inv_map_Δ', map_c₄, j, map_mul, map_pow]

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

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

Разделы

Аффилиация

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