map — Mathlib

English

If φ is homogeneous of degree n and f : R →+* S is a ring homomorphism, then map f φ is homogeneous of degree n.

Русский

Если φ однороден степени n, и f — кольцевое гомоморфизм, то образ φ по f гомогенен той же степени.

LaTeX

$$(IsHomogeneous(\phi, n)) → (IsHomogeneous(map f \phi, n))$$

Lean4

theorem map (hφ : φ.IsHomogeneous n) (f : R →+* S) : (map f φ).IsHomogeneous n := by
  simpa only [one_mul] using hφ.eval₂ _ _ (fun r ↦ isHomogeneous_C _ (f r)) (isHomogeneous_X _)

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