splits_id_iff_splits — Mathlib

English

For a map i, splitting commutes with map under splits on coefficients: splits after map equals splits before map.

Русский

Разложение сохраняется через отображение: разложение после отображения равно разложению до отображения на коэффициентах.

LaTeX

$$splits_id_iff_splits {f : K[X]} : (f.map i).Splits (RingHom.id L) ↔ f.Splits i$$

Lean4

theorem splits_id_iff_splits {f : K[X]} : (f.map i).Splits (RingHom.id L) ↔ f.Splits i := by
  rw [splits_map_iff, RingHom.id_comp]

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