map_invUnitsSub — Mathlib

English

Under a ring hom f, image commutes with invUnitsSub under Units.map.

Русский

При гомоморфизме кольца f отображение совместимо с invUnitsSub через Units.map.

LaTeX

$$map f (invUnitsSub u) = invUnitsSub (Units.map f u)$$

Lean4

theorem map_invUnitsSub (f : R →+* S) (u : Rˣ) : map f (invUnitsSub u) = invUnitsSub (Units.map (f : R →* S) u) :=
  by
  ext
  simp only [← map_pow, coeff_map, coeff_invUnitsSub, one_divp]
  rfl

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