mk0_inj — Mathlib

English

In a group with zero, mk0 is injective on nonzero elements: a ≠ 0, b ≠ 0 implies Units.mk0 a ha = Units.mk0 b hb iff a = b.

Русский

В группе с нулём mk0 инъективна на ненулевых элементах: a ≠ 0, b ≠ 0 ⇒ Units.mk0 a ha = Units.mk0 b hb ⇔ a = b.

LaTeX

$$$\forall a,b\in G_0\, (ha:\, a\neq 0)\,(hb:\, b\neq 0):\ Units.mk0\ a\ ha = Units.mk0\ b\ hb \iff a = b$$$

Lean4

@[simp]
theorem mk0_inj {a b : G₀} (ha : a ≠ 0) (hb : b ≠ 0) : Units.mk0 a ha = Units.mk0 b hb ↔ a = b :=
  ⟨fun h => by injection h, fun h => Units.ext h⟩

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