English
The first n coefficients on degreeLT(n) form a linear equivalence with Fin n → R.
Русский
Первые n коэффициентов на degreeLT(n) образуют линейное эквивалентное отображение с Fin n → R.
LaTeX
$$$\text{degreeLTEquiv}(R,n) :\; \operatorname{degreeLT}_R(n) \cong_{R} \mathbb{F}^n_R$ (linear equivalence with Fin n → R).$$
Lean4
/-- The equivalence between monic polynomials of degree `n` and polynomials of degree less than
`n`, formed by adding a term `X ^ n`. -/
def monicEquivDegreeLT [Nontrivial R] (n : ℕ) : { p : R[X] // p.Monic ∧ p.natDegree = n } ≃ degreeLT R n
where
toFun
p :=
⟨p.1.eraseLead, by
rcases p with ⟨p, hp, rfl⟩
simp only [mem_degreeLT]
refine lt_of_lt_of_le ?_ degree_le_natDegree
exact degree_eraseLead_lt (Polynomial.Monic.ne_zero_of_polynomial_ne hp one_ne_zero)⟩
invFun := fun p =>
⟨X ^ n + p.1, monic_X_pow_add (mem_degreeLT.1 p.2),
by
rw [natDegree_add_eq_left_of_degree_lt]
· simp
· simp [mem_degreeLT.1 p.2]⟩
left_inv := by
rintro ⟨p, hp, rfl⟩
ext1
simp only
conv_rhs => rw [← eraseLead_add_C_mul_X_pow p]
simp [Monic.def.1 hp, add_comm]
right_inv := by
rintro ⟨p, hp⟩
ext1
simp only
rw [eraseLead_add_of_degree_lt_left]
· simp
· simp [mem_degreeLT.1 hp]
