map_equation — Mathlib

English

For an injective f, the mapped equation equals the original equation: equivalence of equations under injective base-change.

Русский

При инъективном f отображённое уравнение равно исходному: равносильность уравнений при инъективном изменении основания.

LaTeX

$$$$ (W'.\\mathrm{map} f).\\mathrm{toJacobian}.\\mathrm{Equation}(f \\circ P) \\iff W'.\\mathrm{Equation} P $$$$

Lean4

@[simp]
theorem map_equation (hf : Function.Injective f) : (W'.map f).toJacobian.Equation (f ∘ P) ↔ W'.Equation P := by
  simp only [Equation, map_polynomial, eval_map, ← eval₂_comp, map_eq_zero_iff f hf]

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