rootSpan_map_toPerfPair — Mathlib

English

The image of the root span under the perf-pair map equals the span generated by the roots range.

Русский

Образ корневого охвата под отображением perfPair равен span, образованному диапазоном корня.

LaTeX

$$$(P.rootSpan R).map P.toPerfPair = span R (range P.root')$$

Lean4

@[simp]
theorem rootSpan_map_toPerfPair : (P.rootSpan R).map P.toPerfPair = span R (range P.root') := by
  rw [rootSpan, Submodule.map_span, ← image_univ, ← image_comp, image_univ, toPerfPair_comp_root]

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