mapDomain_injective — Mathlib

English

An alternate form: Injectivity of mapDomain follows from injectivity of f on coefficients.

Русский

Альтернативная форма: инъективность mapDomain следует из инъективности f на коэффициентах.

LaTeX

$$$ Injective( mapDomain f ) \text{ follows from } Injective f $$$

Lean4

@[to_additive]
theorem mapDomain_injective (hf : Injective f) : Injective (mapDomain (R := R) f) :=
  Finsupp.mapDomain_injective hf

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