of_injective — Mathlib

English

The inclusion map of M into GrothendieckGroup M is injective whenever M is cancellative.

Русский

Включение M в GrothendieckGroup M инъективно тогда, когда M удовлетворяет условию отмены.

LaTeX

$$$\\text{Injective}(\\mathrm{of})$ under $\\text{IsCancelMul}(M)$$$

Lean4

@[to_additive]
theorem of_injective [IsCancelMul M] : Injective (of (M := M)) := fun m₁ m₂ ↦ by
  simp [of, ← mk_one_eq_monoidOf_mk, mk_eq_mk_iff']

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