congr_postcomp — Mathlib

English

If two solutions are equal, postcomposition with a fixed linear map f yields equal postcompositions.

Русский

Если решения совпадают, то их посткомпозиции на фиксированное отображение совпадают.

LaTeX

$$$\text{solution} = \text{solution'} \Rightarrow \text{solution.postcomp } f = \text{solution'.postcomp } f$$$

Lean4

theorem congr_postcomp {solution' : relations.Solution M} (h : solution = solution') (f : M →ₗ[A] N) :
    solution.postcomp f = solution'.postcomp f := by rw [h]

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