English
Same principle as above for injective renaming: deg_w(rename e(P)) = deg_{w∘e}(P).
Русский
То же самое для инъективного переименования: deg_w(rename e(P)) = deg_{w∘e}(P).
LaTeX
$$$\\operatorname{weightedTotalDegree}_w(\\rename_e P) = \\operatorname{weightedTotalDegree}_{w \\circ e} P$$$
Lean4
/-- The submodule of homogeneous `MvPolynomial`s of degree `n`. -/
def homogeneousSubmodule (n : ℕ) : Submodule R (MvPolynomial σ R)
where
carrier := {x | x.IsHomogeneous n}
smul_mem' r a ha c
hc := by
rw [coeff_smul] at hc
apply ha
intro h
apply hc
rw [h]
exact smul_zero r
zero_mem' _ hd := False.elim (hd <| coeff_zero _)
add_mem' {a b} ha hb c
hc := by
rw [coeff_add] at hc
obtain h | h : coeff c a ≠ 0 ∨ coeff c b ≠ 0 := by
contrapose! hc
simp only [hc, add_zero]
· exact ha h
· exact hb h
