English
There exists an instance that endows gradeBy with a gradedMonoid structure using a given f.
Русский
Существует экземпляр, наделяющий gradeBy структурой градуированного моноида с использованием f.
LaTeX
$$$\\text{gradeBy.gradedMonoid}(f)\\;:\\; SetLike.\\,GradedMonoid\\; (gradeBy\\; R\\; f)$$$
Lean4
instance gradedMonoid [AddMonoid M] [AddMonoid ι] [CommSemiring R] (f : M →+ ι) :
SetLike.GradedMonoid (gradeBy R f : ι → Submodule R R[M])
where
one_mem m
h := by
rw [one_def] at h
obtain rfl : m = 0 := Finset.mem_singleton.1 <| Finsupp.support_single_subset h
apply map_zero
mul_mem i j a b ha hb c
hc := by
classical
obtain ⟨ma, hma, mb, hmb, rfl⟩ : ∃ y ∈ a.support, ∃ z ∈ b.support, y + z = c :=
Finset.mem_add.1 <| support_mul a b hc
rw [map_add, ha ma hma, hb mb hmb]
