mul_right — Mathlib

English

If s is nontrivial and t is nonempty, then s * t is nontrivial; the right-multiplicative version of the left variant.

Русский

Если s ненулевое, а t непустое, то s * t ненулево; правая версия по умножению аналогична левой.

LaTeX

$$s.Nontrivial → t.Nonempty → (s * t).Nontrivial$$

Lean4

@[to_additive]
theorem mul_right : s.Nontrivial → t.Nonempty → (s * t).Nontrivial :=
  by
  rintro ⟨a, ha, b, hb, hab⟩ ⟨c, hc⟩
  exact ⟨a * c, mul_mem_mul ha hc, b * c, mul_mem_mul hb hc, by simpa⟩

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