isUnit_map_of_injective — Mathlib

English

If g: A → L is an injective ring homomorphism, then the image of any nonZeroDivisor in A is a unit in L.

Русский

Если g: A → L инъективно, то образ любого ненулевого делителя в A является единицей в L.

LaTeX

$$isUnit_map_of_injective (hg) (y) : IsUnit (g y)$$

Lean4

theorem isUnit_map_of_injective (hg : Function.Injective g) (y : nonZeroDivisors A) : IsUnit (g y) :=
  haveI := g.domain_nontrivial
  IsUnit.mk0 (g y) <| show g.toMonoidWithZeroHom y ≠ 0 from map_ne_zero_of_mem_nonZeroDivisors g hg y.2

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