tmul_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.IsAddUnit.tmul_right {m : M} (hm : IsAddUnit m) (n : N) : IsAddUnit (m ⊗ₜ[R] n) :=
  by
  rw [isAddUnit_iff_exists_neg] at hm ⊢
  have ⟨b, eq⟩ := hm
  exact ⟨b ⊗ₜ[R] n, by rw [← add_tmul, eq, zero_tmul]⟩

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