mulActionBaseChange_smul_zero — Mathlib

English

The actions of S and A commute on the tensor product S ⊗R Ω[A/R].

Русский

Действия S и A коммьютируют друг с другом на тензорном произведении S ⊗R Ω[A/R].

LaTeX

$$$\\text{SMulCommClass } S A\\; (S \\otimes_R \\Omega[A/R]).$$$

Lean4

@[local simp]
theorem mulActionBaseChange_smul_zero (a : A) : a • (0 : S ⊗[R] Ω[A⁄R]) = 0 := by
  rw [← zero_tmul _ (0 : Ω[A⁄R]), mulActionBaseChange_smul_tmul, smul_zero]

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