addLinearEquiv_apply — Mathlib

English

For f ∈ R[X]_{m+n}, the first component equals f %ₘ (X^m).

Русский

Для f ∈ R[X]_{m+n}, первый компонент равен f %ₘ (X^m).

LaTeX

$$$\\text{fst-part} = f \\%_m (X^m).$$$

Lean4

theorem addLinearEquiv_apply {R : Type*} [Ring R] (f) :
    addLinearEquiv R m n f =
      (⟨f %ₘ (X ^ m), addLinearEquiv_apply_fst f ▸ Subtype.prop _⟩,
        ⟨f /ₘ (X ^ m), addLinearEquiv_apply_snd f ▸ Subtype.prop _⟩) :=
  Prod.ext (Subtype.ext <| addLinearEquiv_apply_fst f) (Subtype.ext <| addLinearEquiv_apply_snd f)

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