isLocalHom_expand — Mathlib

English

For a commutative ring R with IsDomain, the expansion by p is a local homomorphism provided p > 0.

Русский

Для коммутативного кольца R, удовлетворяющего IsDomain, расширение по p является локальным гомоморфизмом при p > 0.

LaTeX

$$$$\text{IsLocalHom}(\mathrm{expand}_R(p))$$$$

Lean4

theorem isLocalHom_expand {p : ℕ} (hp : 0 < p) : IsLocalHom (expand R p) :=
  by
  refine ⟨fun f hf1 => ?_⟩
  have hf2 := eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit hf1)
  rw [coeff_expand hp, if_pos (dvd_zero _), p.zero_div] at hf2
  rw [hf2, isUnit_C] at hf1; rw [expand_eq_C hp] at hf2; rwa [hf2, isUnit_C]

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