smul — Mathlib

English

The pure tensors arising as images of tprod generate the entire symmetric power, i.e., they span the space.

Русский

Чистые тензорные единицы, полученные как образы tprod, образуют всю симметрическую степень; они образуют базис пространства.

LaTeX

$$$ \\operatorname{span}_R(\\operatorname{range}(tprod_R)) = \\top $$$

Lean4

theorem smul (r : R) (x y : ⨂[R] _, M) (h : addConGen (Rel R ι M) x y) : addConGen (Rel R ι M) (r • x) (r • y) := by
  induction h with
  | of x y h =>
    cases h with
    | perm e f =>
      apply isEmpty_or_nonempty ι |>.elim <;> intro h
      · convert addConGen (Rel R ι M) |>.refl _
      · let i := Nonempty.some h
        classical
        convert AddConGen.Rel.of _ _ <| SymmetricPower.Rel.perm (R := R) (ι := ι) e <| Function.update f i (r • f i)
        · rw [MultilinearMap.map_update_smul, Function.update_eq_self]
        ·
          simp_rw [Function.update_apply_equiv_apply, MultilinearMap.map_update_smul, ← Function.update_comp_equiv,
            Function.update_eq_self];
          rfl
  | refl => exact AddCon.refl _ _
  | symm => apply AddCon.symm; assumption
  | trans => apply AddCon.trans <;> assumption
  | add => rw [smul_add, smul_add]; apply AddCon.add <;> assumption

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