English
For j ∈ Fin n, the inverse image of inr applied to a basis of the second component maps to the X^j power in the combined space after natAdd.
Русский
Для j ∈ Fin n, образ в обратном направлении inr, применяемый к базису второго компонента, переходит в X^j в объединённом пространстве после natAdd.
LaTeX
$$$(\\text{addLinearEquiv } R\\,m\\,n).symm \\ (\\text{LinearMap.inr } R\\,\\_\\_ (\\text{basis } R\\,n\\,j)) = \\text{basis } R\\,(m+n)\\,(j.natAdd m).$$$
Lean4
theorem addLinearEquiv_apply' {R : Type*} [Ring R] (f) :
((addLinearEquiv R m n f).1 : R[X]) = f %ₘ (X ^ m) ∧ ((addLinearEquiv R m n f).2 : R[X]) = f /ₘ (X ^ m) :=
by
rw [and_comm, eq_comm, eq_comm (b := _ %ₘ _)]
nontriviality R; refine div_modByMonic_unique _ _ (monic_X_pow _) ⟨?_, ?_⟩
· rw [← addLinearEquiv_symm_apply', LinearEquiv.symm_apply_apply]
· rw [degree_X_pow, ← mem_degreeLT]; exact Subtype.prop _
