mt — Mathlib · SciLib

English

If UniqueMul A B a0 b0 holds, and a∈A, b∈B, and (a ≠ a0 ∨ b ≠ b0), then a*b ≠ a0*b0.

Русский

Если UniqueMul A B a0 b0, и a ∈ A, b ∈ B, и (a ≠ a0 ∨ b ≠ b0), то a*b ≠ a0*b0.

LaTeX

$$$\\forall a\\in A\\,\\forall b\\in B\\,(a\\neq a_0 \\lor b\\neq b_0)\\Rightarrow a b \\neq a_0 b_0$$$

Lean4

@[to_additive]
theorem mt (h : UniqueMul A B a0 b0) : ∀ ⦃a b⦄, a ∈ A → b ∈ B → a ≠ a0 ∨ b ≠ b0 → a * b ≠ a0 * b0 := fun _ _ ha hb k ↦
  by
  contrapose! k
  exact h ha hb k

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