Linear independence with MvPolynomial fractions

Stream: Is there code for X?

[Peter Nelson]

How do I prove this? (Or express the same idea more idiomatically)

It says that if a family of vectors is linear independent when viewed as constants in a fraction ring of polynomials, then they are linear independent as plain vectors.

I'm getting confused by all the algebraMaps.

import Mathlib.RingTheory.Localization.FractionRing
import Mathlib.LinearAlgebra.LinearIndependent.Basic
import Mathlib.Algebra.MvPolynomial.CommRing

example {K ι σ : Type*} [Field K] (v₀ : ι → K) (v : ι → FractionRing (MvPolynomial σ K))
    (hv : ∀ i, v i = (algebraMap (MvPolynomial σ K) _) (MvPolynomial.C (v₀ i)))
    (hli : LinearIndependent (FractionRing (MvPolynomial σ K)) v) :
    LinearIndependent K v₀ := by
  sorry

[Eric Wieser]

theorem more_idiomatic {K ι σ : Type*} [Field K] (v₀ : ι → K)
    (hli : LinearIndependent (FractionRing (MvPolynomial σ K)) (fun i => algebraMap _ (FractionRing (MvPolynomial σ K)) (v₀ i))) :
    LinearIndependent K v₀ := by
  refine (hli.restrict_scalars ?_).of_comp (Algebra.linearMap K (FractionRing (MvPolynomial σ K)))
  simp_rw [← Algebra.algebraMap_eq_smul_one]
  exact FaithfulSMul.algebraMap_injective _ _

example {K ι σ : Type*} [Field K] (v₀ : ι → K) (v : ι → FractionRing (MvPolynomial σ K))
    (hv : ∀ i, v i = (algebraMap (MvPolynomial σ K) _) (MvPolynomial.C (v₀ i)))
    (hli : LinearIndependent (FractionRing (MvPolynomial σ K)) v) :
    LinearIndependent K v₀ := by
  have : v = (fun i => algebraMap _ _ (v₀ i)) := by
    ext; simp [hv]
    rfl
  subst this
  apply more_idiomatic _ hli

[Eric Wieser]

So really docs#LinearIndependent.restrict_scalars is the interesting bit

[Jz Pan]

Maybe you can use docs#LinearIndependent.restrict_scalars' ?

[Peter Nelson]

Thanks!