map_cyclotomic — Mathlib

English

The definition of cyclotomic n R commutes with ring homomorphisms: for any ring hom f, map f (cyclotomic n R) = cyclotomic n S.

Русский

Определение cyclotomic n R сохраняется под отображениями колец: map f (cyclotomic n R) = cyclotomic n S.

LaTeX

$$$\operatorname{map} f (\operatorname{cyclotomic} n R) = \operatorname{cyclotomic} n S$$$

Lean4

/-- The definition of `cyclotomic n R` commutes with any ring homomorphism. -/
@[simp]
theorem map_cyclotomic (n : ℕ) {R S : Type*} [Ring R] [Ring S] (f : R →+* S) :
    map f (cyclotomic n R) = cyclotomic n S :=
  by
  rw [← map_cyclotomic_int n R, ← map_cyclotomic_int n S, map_map]
  have : Subsingleton (ℤ →+* S) := inferInstance
  congr!

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