leftDistribMulAction — Mathlib

English

If m is an additive unit in M, then m ⊗ n is an additive unit in M ⊗_R N for any n ∈ N.

Русский

Если m является аддитивной единицей в M, то m ⊗ n является аддитивной единицей в M ⊗_R N для любого n ∈ N.

LaTeX

$$IsAddUnit(m) → ∀ n, IsAddUnit(m ⊗ n)$$

Lean4

instance leftDistribMulAction : DistribMulAction R' (M ⊗[R] N) :=
  have : ∀ (r : R') (m : M) (n : N), r • m ⊗ₜ[R] n = (r • m) ⊗ₜ n := fun _ _ _ => rfl
  { smul_add := fun r x y => TensorProduct.smul_add r x y
    mul_smul := fun r s x =>
      x.induction_on (by simp_rw [TensorProduct.smul_zero]) (fun m n => by simp_rw [this, mul_smul]) fun x y ihx ihy =>
        by
        simp_rw [TensorProduct.smul_add]
        rw [ihx, ihy]
    one_smul := TensorProduct.one_smul
    smul_zero := TensorProduct.smul_zero }

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