map_mem_nthRootsFinset — Mathlib

English

Under a ring homomorphism, images of nthRootsFinset are nthRootsFinset of the image

Русский

При отображении кольца сохраняется множество корней: образ элементов из nthRootsFinset n a лежит в nthRootsFinset n (f a).

LaTeX

$$$0 < n \Rightarrow x \in \operatorname{nthRootsFinset}(n, a) \Rightarrow f(x) \in \operatorname{nthRootsFinset}(n, f(a))$$$

Lean4

theorem map_mem_nthRootsFinset {S F : Type*} [CommRing S] [IsDomain S] [FunLike F R S] [MonoidHomClass F R S] {a : R}
    {x : R} (hx : x ∈ nthRootsFinset n a) (f : F) : f x ∈ nthRootsFinset n (f a) :=
  by
  by_cases hn : n = 0
  · simp [hn] at hx
  · rw [mem_nthRootsFinset <| Nat.pos_of_ne_zero hn, ← map_pow, (mem_nthRootsFinset (Nat.pos_of_ne_zero hn) a).1 hx]

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