English
For mv-polynomials, renaming variables preserves primality: prime of rename p iff prime of p.
Русский
Пременная переименования сохраняет простоту: простота rename p эквивалентна простоте p.
LaTeX
$$Prime (rename p) ⇔ Prime p$$
Lean4
theorem prime_C_iff : Prime (C r : MvPolynomial σ R) ↔ Prime r :=
⟨comap_prime C constantCoeff (constantCoeff_C _), fun hr =>
⟨fun h =>
hr.1 <| by
rw [← C_inj, h]
simp,
fun h =>
hr.2.1 <| by
rw [← constantCoeff_C _ r]
exact h.map _,
fun a b hd => by
obtain ⟨s, a', b', rfl, rfl⟩ := exists_finset_rename₂ a b
rw [← algebraMap_eq] at hd
have : algebraMap R _ r ∣ a' * b' :=
by
convert _root_.map_dvd (killCompl Subtype.val_injective) hd
· simp
· simp
rw [← rename_C ((↑) : s → σ)]
let f := (rename (R := R) ((↑) : s → σ)).toRingHom
exact (((prime_C_iff_of_fintype s).2 hr).2.2 a' b' this).imp (map_dvd f) (map_dvd f)⟩⟩
