Homogeneous polynomials #
A multivariate polynomial φ is homogeneous of degree n
if all monomials occurring in φ have degree n.
Main definitions/lemmas #
IsHomogeneous φ n: a predicate that asserts thatφis homogeneous of degreen.homogeneousSubmodule σ R n: the submodule of homogeneous polynomials of degreen.homogeneousComponent n: the additive morphism that projects polynomials onto their summand that is homogeneous of degreen.sum_homogeneousComponent: every polynomial is the sum of its homogeneous components.
Library notes #
- The
MvPolynomial.weightedGradedAlgebrainstance provides aGradedAlgebrastructure, yielding the isomorphismMvPolynomial σ R ≃ₐ[R] ⨁ m, weightedHomogeneousSubmodule R w mfor a weight functionw. - The special case with
w = 1of the above yields the algebra isomorphismMvPolynomial σ R ≃ₐ[R] ⨁ i, homogeneousSubmodule σ R i.
def
MvPolynomial.IsHomogeneous
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
(n : ℕ)
:
A multivariate polynomial φ is homogeneous of degree n
if all monomials occurring in φ have degree n.
Equations
- φ.IsHomogeneous n = MvPolynomial.IsWeightedHomogeneous 1 φ n
Instances For
@[simp]
theorem
MvPolynomial.weightedTotalDegree_singleton
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
[DecidableEq σ]
(p : MvPolynomial σ R)
:
The degrees of a polynomial p is a special case of the weightedTotalDegree of p where
the weights are singletons containing each variable.
theorem
MvPolynomial.weightedTotalDegree_one
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
:
The totalDegree of a polynomial p is a special case of the weightedTotalDegree of p
where all of the weights are 1.
@[simp]
theorem
MvPolynomial.weightedTotalDegree_piSingle
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
[DecidableEq σ]
(i : σ)
(p : MvPolynomial σ R)
:
The degreeOf a variable i for a polynomial p is a special case of the
weightedTotalDegree of p where i has the only nonzero weight and that weight is 1.
theorem
MvPolynomial.weightedTotalDegree_rename_of_injective
{R : Type u_3}
[CommSemiring R]
{σ : Type u_5}
{τ : Type u_6}
{e : σ → τ}
{w : τ → ℕ}
{P : MvPolynomial σ R}
(he : Function.Injective e)
:
def
MvPolynomial.homogeneousSubmodule
(σ : Type u_1)
(R : Type u_3)
[CommSemiring R]
(n : ℕ)
:
Submodule R (MvPolynomial σ R)
The submodule of homogeneous MvPolynomials of degree n.
Equations
- MvPolynomial.homogeneousSubmodule σ R n = { carrier := {x : MvPolynomial σ R | x.IsHomogeneous n}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
@[simp]
theorem
MvPolynomial.weightedHomogeneousSubmodule_one
(σ : Type u_1)
(R : Type u_3)
[CommSemiring R]
(n : ℕ)
:
@[simp]
theorem
MvPolynomial.mem_homogeneousSubmodule
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(p : MvPolynomial σ R)
:
theorem
MvPolynomial.homogeneousSubmodule_eq_finsupp_supported
(σ : Type u_1)
(R : Type u_3)
[CommSemiring R]
(n : ℕ)
:
While equal, the former has a convenient definitional reduction.
theorem
MvPolynomial.homogeneousSubmodule_fg
(σ : Type u_1)
(R : Type u_3)
[CommSemiring R]
[Finite σ]
(n : ℕ)
:
(homogeneousSubmodule σ R n).FG
theorem
MvPolynomial.homogeneousSubmodule_mul
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(m n : ℕ)
:
theorem
MvPolynomial.homogeneousSubmodule_one_eq_span_X
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
:
theorem
MvPolynomial.isHomogeneous_monomial
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{d : σ →₀ ℕ}
(r : R)
{n : ℕ}
(hn : Finsupp.degree d = n)
:
((monomial d) r).IsHomogeneous n
theorem
MvPolynomial.totalDegree_eq_zero_iff
(σ : Type u_1)
{R : Type u_3}
[CommSemiring R]
(p : MvPolynomial σ R)
:
theorem
MvPolynomial.totalDegree_zero_iff_isHomogeneous
(σ : Type u_1)
{R : Type u_3}
[CommSemiring R]
{p : MvPolynomial σ R}
:
theorem
MvPolynomial.isHomogeneous_of_totalDegree_zero
(σ : Type u_1)
{R : Type u_3}
[CommSemiring R]
{p : MvPolynomial σ R}
:
p.totalDegree = 0 → p.IsHomogeneous 0
Alias of the forward direction of MvPolynomial.totalDegree_zero_iff_isHomogeneous.
@[simp]
theorem
MvPolynomial.isHomogeneous_C
(σ : Type u_1)
{R : Type u_3}
[CommSemiring R]
(r : R)
:
(C r).IsHomogeneous 0
theorem
MvPolynomial.isHomogeneous_zero
(σ : Type u_1)
(R : Type u_3)
[CommSemiring R]
(n : ℕ)
:
IsHomogeneous 0 n
theorem
MvPolynomial.isHomogeneous_one
(σ : Type u_1)
(R : Type u_3)
[CommSemiring R]
:
IsHomogeneous 1 0
theorem
MvPolynomial.isHomogeneous_of_isEmpty
(σ : Type u_1)
(R : Type u_3)
[CommSemiring R]
[IsEmpty σ]
(f : MvPolynomial σ R)
:
f.IsHomogeneous 0
theorem
MvPolynomial.isHomogeneous_X
{σ : Type u_1}
(R : Type u_3)
[CommSemiring R]
(i : σ)
:
(X i).IsHomogeneous 1
theorem
MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(r : R)
(s : σ →₀ ℕ)
:
@[simp]
theorem
MvPolynomial.homogeneousSubmodule_one_pow
{σ : Type u_1}
(R : Type u_3)
[CommSemiring R]
(n : ℕ)
:
theorem
MvPolynomial.IsHomogeneous.coeff_eq_zero
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
{d : σ →₀ ℕ}
(hd : Finsupp.degree d ≠ n)
:
theorem
MvPolynomial.IsHomogeneous.inj_right
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{m n : ℕ}
(hm : φ.IsHomogeneous m)
(hn : φ.IsHomogeneous n)
(hφ : φ ≠ 0)
:
theorem
MvPolynomial.IsHomogeneous.add
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ ψ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
(hψ : ψ.IsHomogeneous n)
:
(φ + ψ).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.sum
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{ι : Type u_5}
(s : Finset ι)
(φ : ι → MvPolynomial σ R)
(n : ℕ)
(h : ∀ i ∈ s, (φ i).IsHomogeneous n)
:
(∑ i ∈ s, φ i).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.mul
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ ψ : MvPolynomial σ R}
{m n : ℕ}
(hφ : φ.IsHomogeneous m)
(hψ : ψ.IsHomogeneous n)
:
(φ * ψ).IsHomogeneous (m + n)
theorem
MvPolynomial.IsHomogeneous.prod
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{ι : Type u_5}
(s : Finset ι)
(φ : ι → MvPolynomial σ R)
(n : ι → ℕ)
(h : ∀ i ∈ s, (φ i).IsHomogeneous (n i))
:
(∏ i ∈ s, φ i).IsHomogeneous (∑ i ∈ s, n i)
theorem
MvPolynomial.IsHomogeneous.C_mul
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{m : ℕ}
(hφ : φ.IsHomogeneous m)
(r : R)
:
(C r * φ).IsHomogeneous m
theorem
MvPolynomial.isHomogeneous_C_mul_X
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(r : R)
(i : σ)
:
(C r * X i).IsHomogeneous 1
theorem
MvPolynomial.IsHomogeneous.pow
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{m : ℕ}
(hφ : φ.IsHomogeneous m)
(n : ℕ)
:
(φ ^ n).IsHomogeneous (m * n)
theorem
MvPolynomial.isHomogeneous_X_pow
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(i : σ)
(n : ℕ)
:
(X i ^ n).IsHomogeneous n
theorem
MvPolynomial.isHomogeneous_C_mul_X_pow
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(r : R)
(i : σ)
(n : ℕ)
:
(C r * X i ^ n).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.eval₂
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
{S : Type u_4}
[CommSemiring R]
[CommSemiring S]
{φ : MvPolynomial σ R}
{m n : ℕ}
(hφ : φ.IsHomogeneous m)
(f : R →+* MvPolynomial τ S)
(g : σ → MvPolynomial τ S)
(hf : ∀ (r : R), (f r).IsHomogeneous 0)
(hg : ∀ (i : σ), (g i).IsHomogeneous n)
:
(MvPolynomial.eval₂ f g φ).IsHomogeneous (n * m)
theorem
MvPolynomial.IsHomogeneous.map
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[CommSemiring R]
[CommSemiring S]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
(f : R →+* S)
:
((map f) φ).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.of_map
{σ : Type u_1}
{R : Type u_3}
{S : Type u_4}
[CommSemiring R]
[CommSemiring S]
{φ : MvPolynomial σ R}
{n : ℕ}
{f : R →+* S}
(hf : Function.Injective ⇑f)
(h : ((map f) φ).IsHomogeneous n)
:
φ.IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.aeval
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
{S : Type u_4}
[CommSemiring R]
[CommSemiring S]
{φ : MvPolynomial σ R}
{m n : ℕ}
[Algebra R S]
(hφ : φ.IsHomogeneous m)
(g : σ → MvPolynomial τ S)
(hg : ∀ (i : σ), (g i).IsHomogeneous n)
:
((MvPolynomial.aeval g) φ).IsHomogeneous (n * m)
theorem
MvPolynomial.IsHomogeneous.neg
{R : Type u_5}
{σ : Type u_6}
[CommRing R]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
:
(-φ).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.sub
{R : Type u_5}
{σ : Type u_6}
[CommRing R]
{φ ψ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
(hψ : ψ.IsHomogeneous n)
:
(φ - ψ).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.totalDegree_le
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
:
The homogeneous degree bounds the total degree.
See also MvPolynomial.IsHomogeneous.totalDegree when φ is non-zero.
theorem
MvPolynomial.IsHomogeneous.totalDegree
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
(h : φ ≠ 0)
:
theorem
MvPolynomial.IsHomogeneous.degree_eq_sum_deg_support
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
{s : σ →₀ ℕ}
(hs : s ∈ φ.support)
:
theorem
MvPolynomial.IsHomogeneous.rename_isHomogeneous
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
{f : σ → τ}
(h : φ.IsHomogeneous n)
:
((rename f) φ).IsHomogeneous n
theorem
MvPolynomial.IsHomogeneous.rename_isHomogeneous_iff
{σ : Type u_1}
{τ : Type u_2}
{R : Type u_3}
[CommSemiring R]
{φ : MvPolynomial σ R}
{n : ℕ}
{f : σ → τ}
(hf : Function.Injective f)
:
theorem
MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous
{R : Type u_3}
[CommSemiring R]
{N : ℕ}
{φ : MvPolynomial (Fin (N + 1)) R}
{n : ℕ}
(hφ : φ.IsHomogeneous n)
(i j : ℕ)
(h : i + j = n)
:
(((finSuccEquiv R N) φ).coeff i).IsHomogeneous j
theorem
MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{n : ℕ}
[hσ : Finite σ]
{p : Polynomial (MvPolynomial σ R)}
(hp : ((optionEquivLeft R σ).symm p).IsHomogeneous n)
(i j : ℕ)
(h : i + j = n)
:
(p.coeff i).IsHomogeneous j
theorem
MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card
{R : Type u_5}
{σ : Type u_6}
[CommRing R]
[IsDomain R]
{F : MvPolynomial σ R}
{n : ℕ}
(hF : F.IsHomogeneous n)
(h : ∀ (r : σ → R), (eval r) F = 0)
(hnR : ↑n ≤ Cardinal.mk R)
:
See MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero
for a version that assumes Infinite R.
theorem
MvPolynomial.IsHomogeneous.funext_of_le_card
{R : Type u_5}
{σ : Type u_6}
[CommRing R]
[IsDomain R]
{F G : MvPolynomial σ R}
{n : ℕ}
(hF : F.IsHomogeneous n)
(hG : G.IsHomogeneous n)
(h : ∀ (r : σ → R), (eval r) F = (eval r) G)
(hnR : ↑n ≤ Cardinal.mk R)
:
See MvPolynomial.IsHomogeneous.funext
for a version that assumes Infinite R.
theorem
MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero
{R : Type u_5}
{σ : Type u_6}
[CommRing R]
[IsDomain R]
[Infinite R]
{F : MvPolynomial σ R}
{n : ℕ}
(hF : F.IsHomogeneous n)
(h : ∀ (r : σ → R), (eval r) F = 0)
:
See MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card
for a version that assumes n ≤ #R.
theorem
MvPolynomial.IsHomogeneous.funext
{R : Type u_5}
{σ : Type u_6}
[CommRing R]
[IsDomain R]
[Infinite R]
{F G : MvPolynomial σ R}
{n : ℕ}
(hF : F.IsHomogeneous n)
(hG : G.IsHomogeneous n)
(h : ∀ (r : σ → R), (eval r) F = (eval r) G)
:
See MvPolynomial.IsHomogeneous.funext_of_le_card
for a version that assumes n ≤ #R.
instance
MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
:
The homogeneous submodules form a graded ring. This instance is used by DirectSum.commSemiring
and DirectSum.algebra.
noncomputable def
MvPolynomial.homogeneousComponent
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
:
homogeneousComponent n φ is the part of φ that is homogeneous of degree n.
See sum_homogeneousComponent for the statement that φ is equal to the sum
of all its homogeneous components.
Instances For
theorem
MvPolynomial.homogeneousComponent_mem
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
:
theorem
MvPolynomial.coeff_homogeneousComponent
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
(d : σ →₀ ℕ)
:
theorem
MvPolynomial.homogeneousComponent_apply
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
:
theorem
MvPolynomial.homogeneousComponent_isHomogeneous
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
:
((homogeneousComponent n) φ).IsHomogeneous n
@[simp]
theorem
MvPolynomial.homogeneousComponent_zero
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
:
@[simp]
theorem
MvPolynomial.homogeneousComponent_C_mul
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
(n : ℕ)
(r : R)
:
theorem
MvPolynomial.homogeneousComponent_eq_zero'
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
(h : ∀ d ∈ φ.support, Finsupp.degree d ≠ n)
:
theorem
MvPolynomial.homogeneousComponent_eq_zero
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(φ : MvPolynomial σ R)
(h : φ.totalDegree < n)
:
theorem
MvPolynomial.sum_homogeneousComponent
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
:
theorem
MvPolynomial.homogeneousComponent_of_mem
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{m n : ℕ}
{p : MvPolynomial σ R}
(h : p ∈ homogeneousSubmodule σ R n)
:
theorem
MvPolynomial.homogeneousComponent_eq_self
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{n : ℕ}
{p : MvPolynomial σ R}
(hp : p.IsHomogeneous n)
:
theorem
MvPolynomial.support_homogeneousComponent
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(n : ℕ)
(p : MvPolynomial σ R)
:
theorem
MvPolynomial.rename_homogeneousComponent
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{τ : Type u_5}
{φ : σ → τ}
(n : ℕ)
(p : MvPolynomial σ R)
:
theorem
MvPolynomial.HomogeneousSubmodule.gradedMonoid
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
:
The homogeneous submodules form a graded ring.
This instance is used by DirectSum.commSemiring and DirectSum.algebra.
@[reducible, inline]
The decomposition of MvPolynomial σ R into homogeneous submodules.
Equations
- MvPolynomial.decomposition = { decompose' := fun (a : MvPolynomial σ R) => MvPolynomial.decompose' R 1 a, left_inv := ⋯, right_inv := ⋯ }
Instances For
@[reducible, inline]
MvPolynomial σ R as a graded algebra, graded by the degree.
We do not make this a global instance because one may want to consider a different
graded algebra structure on MvPolynomial σ R, induced by another weight function.
To make it a local instance, you may use
attribute [local instance] MvPolynomial.gradedAlgebra.
Equations
- MvPolynomial.gradedAlgebra = { toGradedMonoid := ⋯, decompose' := fun (a : MvPolynomial σ R) => MvPolynomial.decompose' R 1 a, left_inv := ⋯, right_inv := ⋯ }
Instances For
theorem
MvPolynomial.decomposition.decompose'_apply
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
(φ : MvPolynomial σ R)
(i : ℕ)
:
theorem
MvPolynomial.decomposition.decompose'_eq
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
:
DirectSum.Decomposition.decompose' = fun (φ : MvPolynomial σ R) =>
(DirectSum.mk (fun (i : ℕ) => ↥(homogeneousSubmodule σ R i)) (Finset.image (⇑Finsupp.degree) φ.support))
fun (m : ↑↑(Finset.image (⇑Finsupp.degree) φ.support)) => ⟨(homogeneousComponent ↑m) φ, ⋯⟩
theorem
MvPolynomial.mem_iff_homogeneousComponent_mem
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{I : Ideal (MvPolynomial σ R)}
(h : Ideal.IsHomogeneous (homogeneousSubmodule σ R) I)
(p : MvPolynomial σ R)
:
theorem
MvPolynomial.homogeneousComponent_mem_of_mem
{σ : Type u_1}
{R : Type u_3}
[CommSemiring R]
{I : Ideal (MvPolynomial σ R)}
(h : Ideal.IsHomogeneous (homogeneousSubmodule σ R) I)
{p : MvPolynomial σ R}
(hp : p ∈ I)
(n : ℕ)
:
theorem
Ideal.span_eq_map_homogeneousSubmodule
{ι : Type u_1}
{R : Type u_2}
[CommSemiring R]
(x : ι → R)
:
Try to use the universal property of the span (e.g., Submodule.span_induction) instead of
this.
theorem
Ideal.span_pow_eq_map_homogeneousSubmodule
{ι : Type u_1}
{R : Type u_2}
[CommSemiring R]
(x : ι → R)
(n : ℕ)
:
span (Set.range x) ^ n = Submodule.map (MvPolynomial.aeval x).toLinearMap (MvPolynomial.homogeneousSubmodule ι R n)
Try to use the universal property of the span (e.g., Submodule.span_induction) instead of
this.
theorem
Ideal.mem_span_pow_iff_exists_isHomogeneous
{ι : Type u_1}
{R : Type u_2}
[CommSemiring R]
{n : ℕ}
(x : ι → R)
(y : R)
:
y ∈ span (Set.range x) ^ n ↔ ∃ (p : MvPolynomial ι R), p.IsHomogeneous n ∧ (MvPolynomial.eval x) p = y
Try to use the universal property of the span (e.g., Submodule.span_induction) instead of
this.
theorem
Ideal.mem_span_iff_exists_isHomogeneous
{ι : Type u_1}
{R : Type u_2}
[CommSemiring R]
(x : ι → R)
(y : R)
:
Try to use the universal property of the span (e.g., Submodule.span_induction) instead of
this.