units_smul — Mathlib

English

If hv is LinearIndependent over R for v, and i is surjective, j is injective, and the scalar compatibility holds, then LinearIndependent over R' of j ∘ v holds.

Русский

Если v линейно независимо над R и i сюръективна, j инъективна, и соблюдается совместимость скаляров, то j ∘ v линейно независимо над R'.

LaTeX

$$LinearIndependent R' (j ∘ v)$$

Lean4

theorem units_smul {v : ι → M} (hv : LinearIndependent R v) (w : ι → Rˣ) : LinearIndependent R (w • v) :=
  by
  rw [linearIndependent_iff''ₛ] at hv ⊢
  intro s g₁ g₂ hgs hsum i
  rw [← (w i).mul_left_inj]
  refine hv s (fun i ↦ g₁ i • w i) (fun i ↦ g₂ i • w i) (fun i hi ↦ ?_) ?_ i
  · simp_rw [hgs i hi]
  · simpa only [smul_eq_mul, mul_smul, Pi.smul_apply'] using hsum

Похожие утверждения