map_b₂ — Mathlib

English

For any W over R and RingHom f: R → A, the b₂ coefficient of the mapped curve equals f applied to b₂: (W.map f).b₂ = f(W.b₂).

Русский

Для любой W над R и гомоморфизма колец f: R → A коэффициент b₂ кривой, полученной после отображения, равен f(b₂): (W.map f).b₂ = f(W.b₂).

LaTeX

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

Lean4

@[simp]
theorem map_b₂ : (W.map f).b₂ = f W.b₂ := by
  simp only [b₂, map_a₁, map_a₂]
  map_simp

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