inv_map_Δ'

Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass

URI: https://scilib.ai/kg/mathlib#WeierstrassCurve.inv_map_Δ'

English

Under a ring hom f, the discriminant inverse maps to the inverse of the discriminant under f:

Русский

При отображении колец f обратное Δ' переходит в обратное Δ' под f.

LaTeX

$$(W.map f).Δ'^{-1} = Units.map f W.Δ'^{-1}$$

Lean4

theorem inv_map_Δ' : (W.map f).Δ'⁻¹ = Units.map f W.Δ'⁻¹ := by simp

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

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

Разделы

Аффилиация

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