map_range_rTensor_subtype_lid — Mathlib

English

For a ∈ A, b ∈ B, m ∈ M, (a ⊗ b) • m equals a • (b • m).

Русский

Для a ∈ A, b ∈ B, m ∈ M выполняется (a ⊗ b) • m = a • b • m.

LaTeX

$$$a \\otimes_R b \\;\\;\\!\\cdot\\;\\; m = a \\;\\cdot\\; (b \\cdot m).$$$

Lean4

theorem map_range_rTensor_subtype_lid {R Q} [CommSemiring R] [AddCommMonoid Q] [Module R Q] {I : Submodule R R} :
    (range <| rTensor Q I.subtype).map (TensorProduct.lid R Q) = I • ⊤ :=
  by
  rw [← map_top, ← map_coe_toLinearMap, ← Submodule.map_comp, map_top]
  refine
    le_antisymm ?_ fun q h ↦
      Submodule.smul_induction_on h (fun r hr q _ ↦ ⟨⟨r, hr⟩ ⊗ₜ q, by simp⟩) (by simp +contextual [add_mem])
  rintro _ ⟨t, rfl⟩
  exact t.induction_on (by simp) (by simp +contextual [Submodule.smul_mem_smul]) (by simp +contextual [add_mem])

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